The shared dataspace approach to concurrent computation: The Swarm programming model, notation, and logic

In the shared dataspace approach to concurrent computation, the concurrent components of programs communicate by manipulating a content-addressable data structure called a dataspace. In this dissertation we study this paradigm by means of a simple model called Swarm.; The Swarm model unifies several computational paradigms into a single framework. It integrates the tuple space communication metaphor of Gelernter's Linda with a computational model inspired by Chandy and Misra's UNITY. Swarm reduces both communication and computation to a single mechanism--the atomic execution of statements called transactions. In a manner similar to production rules, Swarm transactions specify a group of tuple insertions and deletions. Unlike UNITY's static set of statements, Swarm supports a dynamically varying set of transactions. The synchrony relation construct adds further dynamism and flexibility to the Swarm programs. It enables a program to couple individual transactions dynamically into groups; each group is executed atomically as if it were a single transaction.; This dissertation informally specifies the Swarm notation, presents a formal operational model, and defines an axiomatic programming logic--the first such logic for a shared dataspace language. Using a sequence of solutions to the problem of labeling the equal-intensity regions of a digital image, the dissertation explores the impact of Swarm upon programming styles. The dissertation also illustrates use of the programming logic by verifying the correctness of three of the region labeling programs.