CW 549

Bart Jacobs, Frank Piessens
Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions

Abstract

In this short note, we show how ghost fields and fractional permissions can be used to prove fork-join patterns. The approach is a simple port of Owicki and Gries's auxiliary variables-based approach to the setting with dynamic threads, locks, and objects.

report.pdf (145K) / mailto: B. Jacobs