A marriage of Rely/Guarantee and Separation Logic

In the quest for tractable methods for reasoning about concurrent

algorithms both rely/guarantee logic and separation logic have

made great advances. They both seek to tame, or control, the complexity

of concurrent interactions, but neither is the ultimate approach. Rely-guarantee

copes naturally with interference, but its specifications are

complex because they describe the entire state. Conversely separation

logic has difficulty dealing with interference, but its specifications are

simpler because they describe only the relevant state that the program

accesses.

We propose a combined system which marries the two approaches. We

can describe interference naturally (using a relation as in rely/guarantee),

and where there is no interference, we can reason locally (as in separation

logic). We demonstrate the advantages of the combined approach by

verifying a lock-coupling list algorithm, which actually disposes/frees

removed nodes.

In  CONCUR

Publisher  Springer Verlag

Details

TypeInproceedings
Pages256–271
> Publications > A marriage of Rely/Guarantee and Separation Logic