Output details

Elucidating concurrent algorithms via layers of abstraction and reification

<10> The importance here is the general result that rely/guarantee reasoning can tackle race-free programs. O'Hearn's oft-quoted and superficially attractive characterisation is that Separation Logic should be used to show race freedom whereas R/G handles "racy" programs. The example tackled is Simpson's extremely delicate "4-slot" algorithm. The point of the algorithm is to avoid races but the paper shows that R/G reasoning can show race freedom at an abstract level. Coupled with other ideas this is providing a new way of looking at what might be seen as competitive approaches to concurrency.