Avoiding diamonds in desynchronization

H. Beohar, P.J.L. Cuijpers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

The design of concurrent systems often assumes synchronous communication between different parts of a system. When system components are physically apart, this assumption becomes inappropriate. Desynchronization is a technique that aims to implement a synchronous design in an asynchronous manner by placing buffers between the components of the synchronous design. When queues are used as buffers, the so-called ‘diamond property’ (among others) ensures correct operation of the desynchronized design. However, this property is difficult to establish in practice. In this paper, we formally prove that the conditions for desynchronizability can be relaxed, and in particular the diamond property is no longer needed, when half-duplex queues are used as a communication buffer. Furthermore, we discuss how the half-duplex condition can be further relaxed when the diamond property can be partially guaranteed.
Original languageEnglish
Title of host publicationFormal Aspects of Component Software (9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers)
EditorsC.S. Pasareanu, G. Salaun
Place of PublicationBerlin
PublisherSpringer
Pages36-54
ISBN (Print)978-3-642-35860-9
DOIs
Publication statusPublished - 2013
Event9th International Symposium on Formal Aspects of Component Software (FACS 2012), September 12-14, 2012, Mountain View, CA, USA - Mountain View, CA, United States
Duration: 12 Sept 201214 Sept 2012

Publication series

NameLecture Notes in Computer Science
Volume7684
ISSN (Print)0302-9743

Conference

Conference9th International Symposium on Formal Aspects of Component Software (FACS 2012), September 12-14, 2012, Mountain View, CA, USA
Abbreviated titleFACS 2012
Country/TerritoryUnited States
CityMountain View, CA
Period12/09/1214/09/12

Fingerprint

Dive into the research topics of 'Avoiding diamonds in desynchronization'. Together they form a unique fingerprint.

Cite this