[Pl-seminar] PL seminar schedule

[Aaron Turon]

NEU Programming Languages Seminar presents

Ming Fu
Department of Computer Science, USTC

Wednesday, 10/6

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Reasoning about optimistic concurrency using a program logic for history

Optimistic concurrency algorithms provide good performance for
parallel programs but they are extremely hard to reason about. Program
logics such as concurrent separation logic and rely-guarantee
reasoning can be used to verify these algorithms, but they make heavy
uses of history variables which may obscure the high-level intuition
underlying the design of these algorithms. In this paper, we propose a
novel program logic that uses invariants on history traces to reason
about optimistic concurrency algorithms. We use past tense temporal
operators in our assertions to specify execution histories. Our logic
supports modular program specifications with history information by
providing separation over both space (program states) and time. We
prove Michael's non-blocking stack algorithm and show that the
intuition behind such algorithms can be naturally captured using trace
invariants.

URL for the paper: http://flint.cs.yale.edu/flint/publications/roch.html