Lambda the Ultimate

Registration is now open for this year's Code Generation conference. An early-bird booking period runs until 31st March offering significant savings on conference fees.

The conference has a strong practical focus and includes 30+ sessions on many aspects of code generation and model-driven software development.

The event is supported by IASA, OMG, ACCU, SkillsMatter and Cambridge Wireless and members of these organisations receive a further discount on conference participation.

Event sponsors include Microsoft, SoftFluent, itemis and Kennedy Carter.

A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking, Julien Brunel, Damien Doliguez, René Rydhof Hansen, Julia Lawall, Gilles Muller. POPL 2009.

Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of control-flow paths in programs, and indeed an extension of the temporal logic CTL has been applied to the problem of specifying and verifying the transformations commonly performed by optimizing compilers.

Nevertheless, in developing the Coccinelle program transformation tool for performing Linux collateral evolutions in systems code, we have found that existing variants of CTL do not adequately support rules that transform subterms other than the ones matching an entire formula. Being able to transform any of the subterms of a matched term seems essential in the domain targeted by Coccinelle. In this paper, we propose an extension to CTL named CTL-VW (CTL with variables and witnesses) that is a suitable basis for the semantics and implementation of the Coccinelle’s program matching language.

Our extension to CTL includes existential quantification over program fragments, which allows metavariables in the program matching language to range over different values within different control-flow paths, and a notion of witnesses that record such existential bindings for use in the subsequent program transformation process. We formalize CTL-VW and describe its use in the context of Coccinelle. We then assess the performance of the approach in practice, using a transformation rule that fixes several reference count bugs in Linux code

The Coccinelle tool is quite fun to play with. You write things that look like the output of patch, only with some extra patterns and boolean conditions in it, and the tool will go over your C source, find all the source code that matches it, and apply all the changes you've specified. It's open source and available online.

The theory described in this paper is quite fun, too -- the algorithms they describe are (surprisingly) not too complicated and apparently quite speedy.

Hi,

This is to announce the first official release of Dao.

Dao is a simple yet powerful object-oriented programming language with many advanced features including, soft (or optional) typing, BNF-like macro system, regular expression, multi-dimensional numeric array, closure, coroutine, asynchronous function call for concurrent programming etc. Dao provides a rich set of standard data types, methods and libraries. Dao is implemented as a light and efficient virtual machine with very transparent C programming interfaces, which make it easy to extend Dao with C/C++ or embed Dao into C/C++ programs.

There have been a lot of improvements since the last release including: a lot of bug fixing and some broken feature fixing; several large implementation changes to improve the structure and clarity of the codes; and some implementation of new features. For the details, please have a look at: http://www.daovm.net/?page=dao_whats_new.

Besides the improvements to the language and its implementation, the modules, tools, documentations and website associated with this language have also been improved greatly. The documentations are more complete than before, and are prepared in nice formats for easy referencing. A number of demos are also included in the release, including some programs for the The Computer Language Benchmarks Game, which can be tried out just for fun.

One automatic tool (tools/autobind.dao) was developed using Dao itself, and was used to create most of the released Dao extending modules, by generating wrappers directly from the header files of the corresponding C/C++ libraries. This tool could also be used to wrap other C/C++ library as necessary.

A new website that was developed using Dao itself too, has been setup at http://www.daovm.net, and is going to be the new official website of Dao. This new website will be established as a serious platform to promote the spreading of Dao and to grow a community of its users.

Have fun.

Links:
Home: http://www.daovm.net
Document: http://www.daovm.net/?page=document_en
Download: http://www.daovm.net/?page=download_en
Forum: http://www.daovm.net/?forum

(edit: fixed some links)