Local Action Traces and Abstract Concurrent Separation Logic

Add to your list(s) Download to your calendar using vCal

• Steve Brookes, CMU
• Wednesday 07 July 2010, 11:00-12:00
• Small Lecture Room, Microsoft Research, Roger Needham Building, 7 J J Thomson Avenue, Cambridge CB3 0FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Concurrent separation logic is a Hoare-style logic for safe partial correctness of shared-memory parallel programs that operate on mutable state. In prior work we gave a denotational semantics, based on action traces, whose structure directly reflects the underlying RAM model, and we used the semantics to establish soundness of this logic. Later work by Calcagno, O`Hearn and Yang introduced a more general class of state models called separation algebras, designed to abstract away from the RAM and other specific models used elsewhere in work on separation logics. They formulated a notion of local action, represented mathematically as a (non-deterministic) state transformer that mutates state in a local manner. They gave a trace-based semantics, and an abstract version of separation logic, interpreted over arbitrary separation algebras. A major aim of their work was to formulate a semantic model that made ``locality`` explicit in a general, widely applicable manner. Their semantic construction makes several different design choices in contrast to the RAM -based action traces model, leading to some quirks in the modelling of parallel composition. In this paper we present a more straightforward way to design an action trace semantics based on local actions, leading to an elegant generalization 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, including safe total correctness, in addition to safe partial correctness. The model can also be seen to embody Dijkstra`s Principle, that loosely coupled processes should be regarded as independent, except at synchronization points. The adjustments are rather natural, and our semantics can also be used to offer a general soundness proof of abstract concurrent separation logic.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Room, Microsoft Research, Roger Needham Building, 7 J J Thomson Avenue, Cambridge CB3 0FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.