CoLoSL: Concurrent Local Subjective Logic

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

• Azalea Raad (Imperial)
• Friday 24 April 2015, 16:00-17:00
• CS 245.

If you have a question about this talk, please contact Neel Krishnaswami.

A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared state, impeding compositionality. This paper introduces the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the state accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread. This flexibility gives rise to small specifications and, hence, more compositional reasoning for concurrent programs. We demonstrate our reasoning on a range of examples, including a concurrent computation of a spanning tree of a graph.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

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

Note that ex-directory lists are not shown.