Local Action Traces and Abstract Concurrent Separation Logic

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

• Steve Brookes, Carnegie Mellon University and Queen Mary, University of London
• Friday 23 July 2010, 14:00-15:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

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 Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.