A semantic framework for analyzing safe composition of distributed programs
is presented. Its applicability is illustrated by a study of program
composition when communication is reliable but not necessarily FIFO\@. In this
model, special care must be taken to ensure that messages do not accidentally
overtake one another in the composed program. We show that barriers do not
exist in this model. Indeed, no program that sends or receives messages can
automatically be composed with arbitrary programs without jeopardizing their
intended behavior. Safety of composition becomes context-sensitive and new
tools are needed for ensuring it. A notion of sealing is defined, where
if a program $P$ is immediately followed by a program $Q$ that seals $P$ then
$P$ will be communication-closed--it will execute as if it runs in isolation.
The investigation of sealing in this model reveals a novel connection between
Lamport causality and safe composition. A characterization of sealable programs
is given, as well as efficient algorithms for testing if $Q$ seals $P$ and for
constructing a seal for a significant class of programs. It is shown that every
sealable program that is open to interference on $O(n^2)$ channels can be
sealed using O(n) messages.
Description
[cs/0701064] Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels
%0 Generic
%1 engelhardt2007causing
%A Engelhardt, Kai
%A Moses, Yoram
%D 2007
%K composition distributed
%T Causing Communication Closure: Safe Program Composition with Reliable
Non-FIFO Channels
%U http://arxiv.org/abs/cs/0701064
%X A semantic framework for analyzing safe composition of distributed programs
is presented. Its applicability is illustrated by a study of program
composition when communication is reliable but not necessarily FIFO\@. In this
model, special care must be taken to ensure that messages do not accidentally
overtake one another in the composed program. We show that barriers do not
exist in this model. Indeed, no program that sends or receives messages can
automatically be composed with arbitrary programs without jeopardizing their
intended behavior. Safety of composition becomes context-sensitive and new
tools are needed for ensuring it. A notion of sealing is defined, where
if a program $P$ is immediately followed by a program $Q$ that seals $P$ then
$P$ will be communication-closed--it will execute as if it runs in isolation.
The investigation of sealing in this model reveals a novel connection between
Lamport causality and safe composition. A characterization of sealable programs
is given, as well as efficient algorithms for testing if $Q$ seals $P$ and for
constructing a seal for a significant class of programs. It is shown that every
sealable program that is open to interference on $O(n^2)$ channels can be
sealed using O(n) messages.
@misc{engelhardt2007causing,
abstract = {A semantic framework for analyzing safe composition of distributed programs
is presented. Its applicability is illustrated by a study of program
composition when communication is reliable but not necessarily FIFO\@. In this
model, special care must be taken to ensure that messages do not accidentally
overtake one another in the composed program. We show that barriers do not
exist in this model. Indeed, no program that sends or receives messages can
automatically be composed with arbitrary programs without jeopardizing their
intended behavior. Safety of composition becomes context-sensitive and new
tools are needed for ensuring it. A notion of \emph{sealing} is defined, where
if a program $P$ is immediately followed by a program $Q$ that seals $P$ then
$P$ will be communication-closed--it will execute as if it runs in isolation.
The investigation of sealing in this model reveals a novel connection between
Lamport causality and safe composition. A characterization of sealable programs
is given, as well as efficient algorithms for testing if $Q$ seals $P$ and for
constructing a seal for a significant class of programs. It is shown that every
sealable program that is open to interference on $O(n^2)$ channels can be
sealed using O(n) messages.},
added-at = {2012-04-01T14:39:58.000+0200},
author = {Engelhardt, Kai and Moses, Yoram},
biburl = {https://www.bibsonomy.org/bibtex/2e11aee09f09a070ef614f6a4d674f33b/giuliano.losa},
description = {[cs/0701064] Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels},
interhash = {7f88b588a83d36e713e39fb9ebb56f0c},
intrahash = {e11aee09f09a070ef614f6a4d674f33b},
keywords = {composition distributed},
note = {cite arxiv:cs/0701064},
timestamp = {2012-04-01T14:39:58.000+0200},
title = {Causing Communication Closure: Safe Program Composition with Reliable
Non-FIFO Channels},
url = {http://arxiv.org/abs/cs/0701064},
year = 2007
}