Sequential program composition in UNITY

Abstract

Large distributed applications are composed of basic blocks, by using composition operators. In an ideal situation, one should be able to develop and verify each of these basic components by itself, using compositionality theorems of the respective composition operators stating that properties of a composite program can be proved by proving properties of its components. Generally, two forms of distributed program composition can be distinguished: parallel composition and sequential composition. Parallel composition is standard in UNITY [CM89], and is used when two distributed component-programs need to cooperate in one way or another. Compositionality theorems of parallel composition on general progress properties are extensively studied in [CM89, Sin89a, Pra95]. Sequential composition of UNITY programs is not part of core UNITY [CM89]. It can however be very useful when we want a program to work with the results of another program. For example, for the Propogation of Information with Feedback (PIF) protocol [Seg83]: elect a leader ;let the leader be the starter of the PIF protocol In [Mis90b], a brief and intuitive characterisation of sequential composition is given. In this technical report, we shall formally define and model sequential program composition within the HOL-UNITY embedding described in [Pra95, Vos00] In order to do so, we introduce a new type of UNITY programs called UNITY+ programs which consist of sequentially composed UNITY programs. The semantics of a UNITY+ programs is then defined in terms of a UNITY program that models the desired behaviour of the sequential composition. Finally, safety and progress operators are defined for these UNITY+ programs, and compositionality theorems are derived. For those readers not familiar with UNITY and its embedding in HOL, Appendix A contains a brief overview of it. For those readers that are familiar with UNITY, we have compiled an extensive index that should enable the reader to start reading this technical report, looking up desired definitions in a demand-driven way.