Modeling and designing concurrent systems is one of the most challenging tasks faced by software engineers as is evinced by many examples of error-laden large and small-scale concurrent systems. The primary difficulty is the inarticulate characterization of the semantics of concurrent systems. The successful development of concurrent systems requires a clear understanding of the types of relationships that exist between the components found in such systems. Two particularly important relationships found in concurrent systems are the order relation and the containment relation. The order relation represents the relative timing of component actions within a concurrent system and the containment relation facilitates human understanding of a system by abstracting a system's components into layers of visibility. One major consequence of improper management of the order and containment relationships in a concurrent system is deadlock. Deadlock is an undesirable halting of a system's execution and is the most challenging type of concurrent system error to debug. The contents of this publication show that no methodology is currently available that can concisely, accurately and graphically model both the order and containment relations found in complex, concurrent systems. The result of the absence of a method suitable for modeling both order and containment is that analysis of concurrent systems is nearly impossible and the prevention of deadlock is extremely challenging. I created the diposet as a solution to this problem and introduce the diposet in this publication. A diposet is a formal, mathematical structure that is similar in nature to a partially ordered set and is well suited to describing concurrent, computational systems. I define the diposet and show that it uses an order-centric approach that offers insight into the relative timing of events in a concurrent system and allows the specification of containment. The diposet offers an approach that is distinct from traditional formal concurrency methods that instead focus on logic which is non-graphical and often inaccessible to the non-mathematician. The formal structure of a diposet is illustrated through the construction of several proofs and theorems and I provide real world examples to show that the diposet can model a wide variety of communication semantics including synchronous and asynchronous message passing.
By: John S. Davis II
Published in: RC21924 in 2001
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .