Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constructing Weakly Terminating Interface Protocols

Debjyoti Bera, Tim A. C. Willemse

Abstract

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.

Constructing Weakly Terminating Interface Protocols

Abstract

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.
Paper Structure (9 sections, 15 theorems, 3 equations, 9 figures)

This paper contains 9 sections, 15 theorems, 3 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Labeled Portnets and their Mirrors
  4. Well-Formed Labeled Portnets
  5. Weak Termination of Composition of Labeled Portnets
  6. Weak Termination of Composition of Multiple Portnets
  7. Relation to Component Framework.
  8. Application
  9. Conclusion

Key Result

lemma 1

Let $N$ be a labeled portnet and $t, t' \in T$ such that $\mu(t) = \mu(t')$. Then $\lambda(t) = \lambda(t')$.

Figures (9)

  • Figure 1: The Mirrored Portnet Interaction Pattern
  • Figure 2: Labeled Portnets and their Composition
  • Figure 3: Deadlock in a Composition of Labeled Portnet and its Mirror
  • Figure 4: Portnet Properties
  • Figure 5: Well-formed portnet and its well-formed partial mirror portnet
  • ...and 4 more figures

Theorems & Definitions (46)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • lemma 1
  • proof
  • corollary 1
  • definition 7
  • ...and 36 more