Coding Simple Consensus Algorithm

Presented at the October 28, 2011 PRL Seminar

This Friday Bob, Mark and Vincent will illustrate how Event ML and Nuprl cooperate to produce correct-by-construction code for the Simple Consensus Algorithm. This example illustrates many features of Event Logic and of the practical use of Mark's notion of programmable event classes.

We will also illustrate how we can introduce diversity into the code at a high level and multiply it as we compile the protocol to production languages.

This Friday’s seminar will take place in Upson 5126 from Noon-1PM.

PRL Research Meeting: Posting Consensus Material to the Library

Join a discussion with the PRL team.

The PRL seminar for Friday Oct 21 will be a research meeting concerned with how to post proof material for simple consensus to the Library.  We will examine the formal material as written in Nuprl proofs and in EventML and consider the best ways of organizing this material in the library. Rich will display the material interactively to help focus the discussion.

This Friday’s seminar will take place in Upson 5126 from Noon-1PM.

There will be no PRL Seminar this week. We will resume next week Oct 21.

This month's Logical Methods in Computer Science (Vol 7 Issue 2) published an article by the PRL Group. The article Knowledge-Based Synthesis of Distributed Systems Using Event Structures by Mark Bickford, Robert Constable, Joseph Halpern, and Sabina Petride discusses... well rather than try to summarize it, here is the link and abstract:

Link: http://www.lmcs-online.org/ojs/viewarticle.php?id=496&layout=abstract

Abstract

To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.

The PRL Seminar for this Friday, October 7 will be Mark Bickford presenting Alexei Kopylov's work on the Image Type titled: Image Type: A New Type Constructor.

The seminar will take place in Upson 5126 from Noon-1PM.

Jim