Graphical Models of Separation Logic

Date Added: Jun 2009
Format: PDF

Graphs are used to model control and data flow among events occurring in the execution of a concurrent program. The authors' treatment of data flow covers both shared storage and external communication. Nevertheless, the laws of Hoare and Jones correctness reasoning remain valid when interpreted in this general model. In this paper, they present a trace semantics based on graphs: nodes represent the events of a program's execution, and edges represent dependencies among the events. The style is reminiscent of partially ordered models, though they do not generally require properties like transitivity or acyclicity.