Current events

From The Programming Languages and Systems Research Group
Revision as of 12:25, 18 September 2007 by Muehlber (talk | contribs)

Jump to: navigation, search

Friday, 21 September Neil Mitchell: "Uniform Boilerplate and List Processing"
Friday, 21 September Matthew Naylor: "Finding inputs that reach a target expression"
Friday, 21 September Neil Mitchell: "Supero: Making Haskell Faster"

Regular group meetings

During term time we meet each week to discuss topical issues. A discussion may be initiated by a short talk given by a member or guest of the group.

Talks can be booked by contacting Jan Tobias Muehlberg. Suitable topics are:

  • Any subject related to programming languages and systems
  • Work in progress to discuss, or ideas you've been mulling over
  • Reports on a paper you read, a recent conference, workshop or visit to another institution, which you think may interest other members of the group
  • Practice for a talk you will be giving at a conference or workshop to obtain feedback from your colleagues

Details of meetings in previous years are available.

Meetings During the Summer Break 2007

Monday, 23 July Borzoo Bonakdarpour (Michigan State University): "Exploiting Symbolic Techniques in Automated synthesis of Distributed Programs with Large State Space"
11:15 -- 12:15, CS202J Abstract: Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time complexity of their decision procedures and also high space complexity known as the state explosion problem. Symbolic techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy the state explosion problem and time complexity of decision procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond 10^30) is handled during synthesis.

Friday, 21 September Neil Mitchell: "Uniform Boilerplate and List Processing"
13:20 -- 14:00, CS202J Abstract: Generic traversals over recursive data structures are often referred to as boilerplate code. The definitions of functions involving such traversals may repeat very similar patterns, but with variations for different data types and different functionality. Libraries of operations abstracting away boilerplate code typically rely on elaborate types to make operations generic. The motivating observation for this paper is that most traversals have value-specific behaviour for just one type. We present the design of a new library exploiting this assumption. Our library allows concise expression of traversals with competitive performance.

Friday, 21 September Matthew Naylor: "Finding inputs that reach a target expression"
14:00 -- 14:20, CS202J Abstract: We present an automated program analysis, called Reach, to compute program inputs that cause evaluation of explicitly-marked target expressions. Reach has a range of applications including property refutation, assertion breaking, program crashing, program covering, program understanding, and the development of customised data generators. Reach is based on lazy narrowing, a symbolic evaluation strategy from functional-logic programming.

We use Reach to analyse a range of programs, and find it to be a useful tool with clear performance benefits over a method based on exhaustive input generation. We also explore different methods for bounding the search space, the selective use of breadth-first search to find the first solution quickly, and techniques to avoid evaluation that is unnecesary to reach a target.

Friday, 21 September Neil Mitchell: "Supero: Making Haskell Faster"
14:20 -- 15:00, CS202J Abstract: Haskell is a functional language, with features such as higher order functions and lazy evaluation, which allow succinct programs. These high-level features are di±cult for fast execution, but GHC is a mature and widely used optimising compiler. This paper presents a whole-program approach to optimisation, which produces speed improvements of between 10% and 60% when used with GHC, on eight benchmarks.

The list above contains only talks for which at least a speaker and a title are available. The full schedule with incomplete talks and empty slots is available under Meetings During the Summer Break 2007.

Other events

Thursday, 31 August 2006 Jonathan Ezekiel: "Can Saturation be Parallelised? On the Parallelisation of a Symbolic State-Space Generator"
14:430 -- 15:00, PDMC, Bonn (satellite of CONCUR) Abstract: Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models.

This paper explores whether event locality can be utilised to efficiently parallelise Saturation on shared-memory adrchitectures. Conceptually, we propose to parallelise the firing of events within a decision diagram node, which is technically realised via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core. (Joint work with Gerald Luettgen and Radu Siminiceanu)

Sunday, 27 August 2006 Jan Tobias Muehlberg: "BLASTing Linux Code"
About 11:45, FMICS, Bonn (satellite of CONCUR) Abstract: Computer programs can only run reliably if the underlying operating system is free of errors. In this paper we evaluate, from a practitioners point of view, the utility of the popular software model checker BLAST for revealing errors in Linux kernel code. The emphasis is on important errors related to memory safety in and locking behaviour of device drivers. Our conducted case studies show that, while BLAST's abstraction and refinement techniques are efficient and powerful, the tool has deficiencies regarding usability and support for analysing pointers, which are likely to prevent kernel developers from using it. (Joint work with Gerald Luettgen)

Links: slides, paper and additional material

Sunday, 2 April 2006 Greg Manning: "The York Abstract Machine"
About 2pm, GT-VMT, Vienna (satellite of ETAPS) Abstract: We introduce the York Abstract Machine (YAM) for implementing the graph programming language GP and, potentially, other graph transformation languages. The advantages of an abstract machine over a direct interpreter for graph transformation rules are better efficiency, use as a common target for compiling both future versions of GP and other languages, and portability of GP programs to different platforms.