A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency require reasoning about static global shared resource, impeding compositionality. This paper introduces 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.
Thu 16 Apr Times are displayed in time zone: (GMT) Azores change
|14:00 - 14:30|
|14:30 - 15:00|
|15:00 - 15:30|
|15:30 - 16:00|