BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Local Action Traces and Abstract Concurrent Separation Logic - Ste
 ve Brookes\, CMU
DTSTART:20100707T100000Z
DTEND:20100707T110000Z
UID:TALK25413@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* Concurrent separation logic is a Hoare-style logic
  for safe partial correctness of shared-memory parallel programs that oper
 ate on mutable state. In prior work we gave a denotational semantics\, bas
 ed on action traces\, whose structure directly reflects the underlying RAM
  model\, and we used the semantics to establish soundness of this logic. L
 ater work by Calcagno\, O`Hearn and Yang introduced a more general class o
 f state models called separation algebras\, designed to abstract away from
  the RAM and other specific models used elsewhere in work on separation lo
 gics. They formulated a notion of local action\, represented mathematicall
 y as a (non-deterministic) state transformer that mutates state in a local
  manner. They gave a trace-based semantics\, and an abstract version of se
 paration logic\, interpreted over arbitrary separation algebras. A major a
 im of their work was to formulate a semantic model that made ``locality`` 
 explicit in a general\, widely applicable manner. Their semantic construct
 ion makes several different design choices in contrast to the RAM-based ac
 tion traces model\, leading to some quirks in the modelling of parallel co
 mposition. In this paper we present a more straightforward way to design a
 n action trace semantics based on local actions\, leading to an elegant ge
 neralization of our prior model that makes sense over arbitrary separation
  algebras. The new model can easily be extended (by incorporating infinite
  traces) to support reasoning about safety and liveness properties\, inclu
 ding safe total correctness\, in addition to safe partial correctness. The
  model can also be seen to embody Dijkstra`s Principle\, that loosely coup
 led processes should be regarded as independent\, except at synchronizatio
 n points. The adjustments are rather natural\, and our semantics can also 
 be used to offer a general soundness proof of abstract concurrent separati
 on logic.
LOCATION:Small Lecture Room\, Microsoft Research\, Roger Needham Building\
 , 7 J J Thomson Avenue\, Cambridge CB3 0FB
END:VEVENT
END:VCALENDAR