Difference between revisions of "Current events"

From The Programming Languages and Systems Research Group
Jump to: navigation, search
(Meetings in Summer 2007)
Line 27: Line 27:
 
Details of [[Meetings| meetings in previous years]] are available.
 
Details of [[Meetings| meetings in previous years]] are available.
  
== Meetings in Summer 2007 ==  
+
== Meetings During the Summer Break 2007 ==  
  
{{EListEntry|322a|Thursday, 03 May|12:20 -- 12:40, CS202J|Ben Mitchel|Animating Simulated Annealing with Lego Mindstorms|This project explores the physical animation of simulated annealing using Lego Mindstorms, and assesses the suitability of this approach to algorithm animation for use as an interactive teaching aid.}}
+
{{EListEntry|331|Monday, 23 July|11:15 -- 12:15, CS202J|Borzoo Bonakdarpour (Michigan State University)|Exploiting Symbolic Techniques in Automated synthesis of Distributed Programs with Large State Space|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.}}
  
{{EListEntry|322b|Thursday, 03 May|12:40 -- 13:00, CS202J|Ian Boden|Animation of Garbage Collection Algorithms using Lego Mindstorms|My project investigates the use of Lego Mindstorms for educating students about Garbage Collection algorithms. It concentrates on producing a tool for demonstration and independent learning which is as capable of educating as standard methods with the advantage of making the topic more exciting for the students.}}
+
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_Term_Break_2007|Meetings During the Summer Break 2007]].
 
 
{{EListEntry|325|Thursday, 24 May|12:15 -- 13:15, CS202J|Malcolm Wallace|Functional Programming and Visualisation: A Lazy PolyTypic Grid|This talk will give an overview of the Lazy Polytypic Grid project,and outline some of our early results.  Our aim is to explore how to make existing well-known visualisation algorithms (e.g. volumetric surface extraction):
 
 
 
* lazy, so that the whole dataset is not required all at once;
 
* datatype-generic (polytypic), so that the algorithm is independent of the original dataset storage format, including questions of      irregular and unstructured sampling;
 
* grid-enabled, such that it is possible to distribute the processing tasks across a heterogeneous network of machines, harnessing any implicit parallelism in the algorithms to speed up the calculation for huge datasets.}}
 
 
 
{{EListEntry|326|Thursday, 31 May|12:15 -- 13:15, CS202J|Neil Mitchell|Fastest Lambda First|Haskell programs are often very succinct, but what they gain in beauty they can sometimes loose in speed. Work on the GHC compiler has enabled Haskell programs to perform at C speeds, or faster in some cases, but at the cost of using a lower-level style of Haskell.
 
 
 
This talk introduces a new technique for optimisation, which attempts to eliminate any overhead from an algorithm. The idea relies on the first-order transformation presented last term, and attempts to remove all data and higher-order functions from a program. With the techniques presented Haskell can remain beautiful, and perform at the same speed as C.
 
 
 
Links: [http://www.cs.york.ac.uk/plasma/talkrelated/326.pdf slides] (PDF)}}
 
 
 
{{EListEntry|327|Thursday, 07 June|12:15 -- 13:15, CS202J|Colin Runciman|Programming with Sets -- Specification and Refinement|}}
 
 
 
{{EListEntry|328|Thursday, 14 June|12:15 -- 13:15, CS202J|Ian Toyn|An Update on the ISO Z Standard and Tools|The speaker holds the position of Project Editor for the ISO Z standard.  The talk will present a paper that was written for a proposed forthcoming Z User Meeting (ZUM). The paper provides a commentary on the recently approved first Technical Corrigendum to the first edition of the Z standard. (A Technical Corrigendum corrects defects in a standard.) The paper also reviews the conformance (or otherwise) to the standard of some widely-used Z tools, as summarised by the tool builders who are listed as co-authors.
 
 
 
The ZUM audience can be assumed to know Z, so for this PLASMA talk to be good practice, I hope I don't have to weaken that assumption very much, but feel free to ask questions.
 
 
 
''Joint work with Rob Arthan, Leo Freitas, Tim Miller and Mark Saaltink.''}}
 
 
 
{{EListEntry|329|Thursday, 21 June|12:15 -- 13:15, CS202J|Gerald Lüttgen|Parallelising Symbolic State-Space Generators: Frustration and Hope|Due to the irregular nature of the task, efficient algorithms for symbolic state-space generation are notoriously hard to parallelise. This talk explores two different strategies for parallelising and implementing one such algorithm, Saturation, on multi-core PCs: one strategy employs the parallel language Cilk, while the other uses a thread pool implemented in Pthreads.
 
 
 
I will analyse the underlying parallel overheads, present experimental results and argue their relevance.  The conclusions will give room for both frustration and hope regarding the parallelisability of symbolic model checkers on shared-memory architectures.
 
 
 
The research on which this talk is based is funded by the EPSRC under grant no. GR/S86211/01: "New-Generation Symbolic Model Checkers for Verifying Asynchronous Systems".}}
 
 
 
{{EListEntry|330|Thursday, 28 June|12:15 -- 13:15, CS202J|Jonathan Ezekiel|Parallelising Symbolic State-Space Generators|Symbolic state-space generators are notoriously hard to parallelise, largely due to the irregular nature of the task. Parallel languages such as Cilk, tailored to irregular problems, have been shown to offer efficient scheduling and load balancing.  This paper explores whether Cilk can be used to efficiently parallelise a symbolic state-space generator on a shared-memory architecture. We parallelise the Saturation algorithm implemented in the SMART verification tool using Cilk, and compare it to a parallel implementation of the algorithm using a thread pool. Our experimental studies on a dual-processor, dual-core PC show that Cilk can improve the run-time efficiency of our parallel algorithm due to its load balancing and scheduling efficiency. We also demonstrate that this incurs a significant memory overhead due to Cilk's inability to support pipelining, and conclude by pointing to a possible future direction for parallel irregular languages to include pipelining.
 
 
 
''A paper to be presented at CAV 2007.''}}
 
 
 
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_in_Summer_2007|Meetings in Summer 2007]].
 
  
 
== Other events ==
 
== Other events ==

Revision as of 16:31, 17 July 2007


Thursday, 24 May Malcolm Wallace: "Functional Programming and Visualisation: A Lazy PolyTypic Grid"
Thursday, 31 May Neil Mitchell: "Fastest Lambda First"
Thursday, 07 June Colin Runciman: "Programming with Sets -- Specification and Refinement"
Thursday, 14 June Ian Toyn: "An Update on the ISO Z Standard and Tools"
Thursday, 21 June Gerald Lüttgen: "Parallelising Symbolic State-Space Generators: Frustration and Hope"
Thursday, 28 June Jonathan Ezekiel: "Parallelising Symbolic State-Space Generators"



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.

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.