Localities and Failures
Identifieur interne : 001544 ( Crin/Corpus ); précédent : 001543; suivant : 001545Localities and Failures
Auteurs : R. Amadio ; S. PrasadSource :
Abstract
We present a simple extension of the \pi-calculus with located actions and channels and with location names as first-class data, which models the notion of locality and failure present in the higher-order, distributed programming language Facile. The interaction between localities and failures distinguishes our approach from previous ones where the notion of locality is considered in isolation. We argue that the combination of these two features leads, at least from the distributed programming viewpoint, to a more natural semantics. We then discuss the translation of this calculus into a standard simply-sorted \pi-calculus and show its adequacy with respect to a barbed bisimulation based semantics. In the translation each location is represented by a special process which interacts, by means of a simple protocol, with any process of the original program that wants to access resources depending on that location. We also apply our translation in the verification of a very simple fault-tolerant program. Thus, we support the view that --- at least in theory --- reasoning about such distributed applications can be carried out in the familiar interleaving semantics of the \pi-calculus.
Links to Exploration step
CRIN:amadio94cLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="35">Localities and Failures</title></titleStmt><publicationStmt><idno type="RBID">CRIN:amadio94c</idno><date when="1994" year="1994">1994</date><idno type="wicri:Area/Crin/Corpus">001544</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Localities and Failures</title><author><name sortKey="Amadio, R" sort="Amadio, R" uniqKey="Amadio R" first="R." last="Amadio">R. Amadio</name></author><author><name sortKey="Prasad, S" sort="Prasad, S" uniqKey="Prasad S" first="S." last="Prasad">S. Prasad</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4163">We present a simple extension of the \pi-calculus with located actions and channels and with location names as first-class data, which models the notion of locality and failure present in the higher-order, distributed programming language Facile. The interaction between localities and failures distinguishes our approach from previous ones where the notion of locality is considered in isolation. We argue that the combination of these two features leads, at least from the distributed programming viewpoint, to a more natural semantics. We then discuss the translation of this calculus into a standard simply-sorted \pi-calculus and show its adequacy with respect to a barbed bisimulation based semantics. In the translation each location is represented by a special process which interacts, by means of a simple protocol, with any process of the original program that wants to access resources depending on that location. We also apply our translation in the verification of a very simple fault-tolerant program. Thus, we support the view that --- at least in theory --- reasoning about such distributed applications can be carried out in the familiar interleaving semantics of the \pi-calculus.</div></front></TEI><BibTex type="inproceedings"><ref>amadio94c</ref><crinnumber>94-R-347</crinnumber><category>3</category><equipe>EURECA</equipe><author><e>Amadio, R.</e><e>Prasad, S.</e></author><title>Localities and Failures</title><booktitle>{Proceedings FST-TCS, Madras}</booktitle><year>1994</year><volume>880</volume><series>Lecture Notes in Computer Science</series><pages>205-216</pages><publisher>Springer Verlag</publisher><abstract>We present a simple extension of the \pi-calculus with located actions and channels and with location names as first-class data, which models the notion of locality and failure present in the higher-order, distributed programming language Facile. The interaction between localities and failures distinguishes our approach from previous ones where the notion of locality is considered in isolation. We argue that the combination of these two features leads, at least from the distributed programming viewpoint, to a more natural semantics. We then discuss the translation of this calculus into a standard simply-sorted \pi-calculus and show its adequacy with respect to a barbed bisimulation based semantics. In the translation each location is represented by a special process which interacts, by means of a simple protocol, with any process of the original program that wants to access resources depending on that location. We also apply our translation in the verification of a very simple fault-tolerant program. Thus, we support the view that --- at least in theory --- reasoning about such distributed applications can be carried out in the familiar interleaving semantics of the \pi-calculus.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001544 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001544 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:amadio94c
|texte= Localities and Failures
}}
| This area was generated with Dilib version V0.6.33. |  |