VR2012

VR2012 -- common information for the CSE dept. about VR 2012

Planning page for the VR application round 2012.

We want to work towards 2012-04-01 as an internal deadline for the grant applications (the "hard" deadline is 2012-04-12 - just after easter).

Common repository: (the ST division git repo)

  git clone remote12.chalmers.se:/chalmers/groups/cse-set/gitroot
  cd gitroot/Proposals/VR

Create your own application in a subdirectory there (like JP/ for Jean-Philippes application). There is also a Notes/ directory with some meeting notes.

First general VR planning meeting: Thursday 2012-03-08, 10.00, in 8103 (by the lunchroom).

Second meeting (mainly about continued funding for the multi-project grant.

Abstracts

Emil

Title: DSL implementation made easy

I would like to work on making it dead easy to implement good DSLs. This involves

Combining the advantages of internal and external DSLs (i.e. embedded implementation but with nicer surface syntax towards the user)
Continue developing Syntactic, making it easier to use

As a concrete application, I would like to work on hardware/software co-design in Feldspar. This is likely to affect the language and its implementation in interesting ways, so it will provide a good case for testing the general methods.

I suspect that hardware generation from Feldspar is an interesting field on its own. It probably requires methods (abstract interpretation, formal verification, testing) for taming the dynamic aspects of Feldspar. I'm not sure whether or not this should be part of the application.

Meng

Title: Good Feedback for DSELs

DSELs are usually considered as a “lightweight” approach to language design and implementation. Manifested as a library, a DSEL inherits the expressiveness of the host language, and readily lends itself to experimentation and customization. Through careful designing, a domain specific embedded compiler may produce code that performs on par with hand-written benchmarks in term of performance. On the other hand, deep embedding of this kind further reduces the already modest ability of embedded languages to provide helpful feedback to users. Messages arise from the generated code reveal details of an implementation, which are often incomprehensible to the users.

The same problem exists in non-embedded language implementations too, and compiler writers are often willing to go a long way to circumvent it. For example in GHC, type checking is performed in the very beginning of the compilation process for the purpose of good error messages. As a result, the handful of typing rules sufficient for the desugared core language explode to scores. This is a high price to pay and is not always applicable. For example, any feedback on the effect of optimizations has to be done retrospectively from the optimized code. Thus, source information has to flow downwards through program transformations, and feedback from the translated program has to flow upwards.

We have carried out some initial studies of this problem in Feldspar. Our current implementation annotates various marked source expressions with their locations, propagates the annotations through program transformations, and presents the source locations as origins of the generated code blocks. The result is encouraging; despite large differences in structure between the source and the generated code, precise source origins can be identified in majority of the cases. We plan to develop the method further along different directions. In particular, we would like to be able to flow information from the generated code back to the source. This has a number of advantages: in situations where the users are expected to work on the domain level only, feedback can be viewed in the source; in other situations where the users are to improve the source programs by inspecting the generated code, it is more desirable to be able to point to blocks in the generated code and identify the source locations, instead of trying to speculatively marking source expressions for annotations, and hope the transformations of the expressions to hit the targets.

To achieve this, program transformations need to be bidirectionalized in a way that the generated code annotated with feedback information can be used to produce source code. Our rich experiences in bidirectional programming will help here. In general, bidirectionalizing programs is a difficult task, and as a result, the class of programs can be handled is usually very restricted. Yet in the specific case investigated here, we are optimistic, because the annotations can be designed in a way that does not alter the structures of the ASTs. In bidirectional programming terminology, changing such annotations constitute to restricted updates, which simplifies the task of regenerating the input from the changed output. We will focus on the modeling of different types of feedback, including error messages, optimization results, profiling information etc., and the way annotations interact with program transformations: the adding of annotations should ideally induce no or little change to existing transformations.

In this project, we will

Model various feedback as part of the ASTs (related to Syntactic)
Investigate the effect of such modelling on existing program transformations (may involve the designing of another DS(E)L for program transformations)
Design suitable bidirectionalization techniques

Remark: My individual proposal will be more about technical advances of bidirectionalization techniques. The plan is to connect it with the group proposal by applying the techniques to DSEL designs. As neither side is fixed yet, I will be happy to adapt this plan as we progress.

JP

Title: Mathematically-Structured Parallel Programming

Until recently, much of the parallel-programming was conducted in an ad-hoc way: for each problem, a new parallel algorithm was devised from scratch.

Recently, Google has popularised another approach, via their map-reduce architecture. If a computation is structured as repeated application (reduce, or fold) of an associative operator (monoid), it can then be run in parallel, and can be scaled up, virtually without limit. The same approach is supported in the Fortress programming language. The lesson to take home is that parallel computers can be modeled mathematically as functions that can only such particular folds.

The map-reduce approach is extremely generic: it can in principle be applied to any problem. This is very powerful, it also means that programmers are given little support for their specific applications. Thus, we propose to build upon this generic framework and construct more specialised versions of the map-reduce approach, not based on freely-chosen monoids, but on more specific mathematical structures. Groups, Abelian groups, rings, etc. come to mind.

Additionally, we want to help programmers using the framework to show their programs correct. Here, we will build upon random testing on the one hand, and proof assistants on the other. Our plan is to build specific libraries, for both frameworks, which take care of (a part of) the burden of proof in place of the programmer. In the case of proof assistants, we will provide, alongside the library of program skeletons, a library of proof skeletons, which can be filled with the portions of the proofs specific to each application. Similarly, we will provide testing tools to check the properties required, which may be used if correctness is a secondary concern or as a first step before full proofs are written.