A Hoare logic for dynamic networks of asynchronously communicating deterministic processes

摘要

This paper introduces a compositional Hoare logic for reasoning about the partial correctness and absence of deadlock of a certain class of programs. Considered are programs that describe networks composed of a dynamically evolving collection of processes which are all executing in parallel, and which know each other by maintaining and passing around process-references via an asynchronous communication mechanism based on (unbounded) FIFO buffers. The Hoare logic formalizes reasoning about such dynamic networks on an abstraction level that is at least as high as that of the programming language. This means that the only operations on 'pointers' (that is, references to processes) are testing for equality and dereferencing. Moreover, in a given state of the system, it is only possible to mention the processes that exist in that state. Processes that have not (yet) been created do not play a role. Soundness and completeness of the logic is proved with respect to a compositional characterization of the initial/final state semantics of programs. This characterization generalizes the compositional semantics of deterministic Kahn (data-flow) networks (where the number of processes and communication structure is fixed).