MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

CoLoSL: Concurrent Local Subjective Logic

Azalea Raad
Imperial College London
SWS Colloquium
SWS, RG1, MMCI  
MPI Audience
English

Date, Time and Location

Monday, 15 December 2014
14:00
90 Minutes
E1 5
029
Saarbrücken

Abstract

A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. When the footprints of threads overlap with each other, existing program logics require reasoning about static global shared resource which impedes compositionality. We introduce the program logic of 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 global shared resource accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread, thus allowing for truly compositional proofs for shared-memory concurrency.

Contact

Claudia Richter
0681 9303 9103
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
112
passcode not visible
logged in users only

Carina Schmitt, 12/15/2014 14:01
Claudia Richter, 12/15/2014 09:27 -- Created document.