|M.Sc Student||Guralnik Elena|
|Subject||Safe Composition of Distributed Programs|
|Department||Department of Electrical Engineering||Supervisor||Professor Yoram Moses|
|Full Thesis text|
One of the important aspects in verification of distributed programs is safe program composition. Much of the distributed algorithms literature is devoted to solutions of individual tasks, but composing such solutions is not automatically guaranteed to maintain their correctness and their intended behavior. The fundamental question "when is program Q, executed immediately after program P, guaranteed not to interfere with P and be safe from interference by P?" was recently studied and answered by Engelhardt and Moses for a restricted class of programs - balanced straight-line programs - in a model with asynchronous, reliable but non-FIFO communication. They showed a very close connection between safe composition and Lamport causality in such a setting. In this work the study of safe composition with reliable non-FIFO channels is extended to a wider class of programs, namely - balanced branching programs. For this class of programs, Lamport causality is no longer sufficient for characterizing safe composition. Instead, I provide a knowledge-based characterization that in a precise sense, generalizes the former analysis. In order to state and prove this characterization a framework for defining knowledge in an open system is provided, in which little is assumed about what comes before, or goes after, the program being studied.