A principal difficulty in the development of high-assurance software is to safely accommodate concurrency and synchronization. The propensity for concurrency to engender state-explosion confounds verification, and the tendency for synchronization logic to be interleaved with "functional" code complicates understanding and maintenance. Thus, development and long-term maintenance of high-assurance software requires design artifacts over which verification is feasible and processes that use these artifacts to maintain separation of concerns in the implementation.
This project aims to achieve these goals. Specifically, it explores a design-for-verification (D4V) approach based on synchronization contracts, which provides the high level of abstraction needed to support verification while maintaining a good separation of synchronization and functional concerns. We are developing programming systems that leverage contract awareness for analysis; to automate the generation of models from design artifacts, (e.g., UML diagrams); and to separate synchronization and functional concerns. We are conducting these explorations in the context of an existing software baseline.
The project also involves development of undergraduate courses in concurrent systems design, model-based software engineering, and D4V. One benchmark is the extent to which undergraduates are able to design and verify contract-aware programs using the tools and methods developed under this grant.
The expressive power and performance gains promised by multi-threaded software comes at the expense of increased complexity. Without proper synchronization, multiple threads may concurrently access the same shared object, producing a race condition, and incorrect synchronization logic can lead to starvation and/or deadlock. Moreover, because synchronization policies and decisions are difficult to localize within software modules, concurrency confounds the development of reusable software. This project developed a model of synchronization contracts for object-oriented languages that addresses this complexity, and validated benefits of this model. Called the Synchronization Units Model (Szumo), the model's key benefits are increased design transparency, separation of synchronization code from functional code, and enhanced extensibility and maintenance. Separating synchronization code from functional code simplifies programming, and localizing synchronization contracts in module interfaces simplifies reasoning about synchronization errors. In this project, we demonstrated that, although the full Szumo negotiation algorithm does not scale well under high contention when compared with hand-optimized solutions, a restricted version of this algorithm reduces contention when compared to two common synchronization policies. This restricted algorithm is well suited to the IP telecommunication services domain. We used it to demonstrate that performance of contract-based automatic synchronization could be very close to that of an optimized manually synchronized implementation of an IP telecommunications service. Our paper on synchronization issues for IP telecommunications services was circulated to the expert group for SIP Servlet API, the current industry standard for deployment of Voice Over IP (VoIP) service, when it was actively debating a specification for a threading model for the standard. Due to our findings, the expert group decided that JSR 289 should not mandate any particular threading model (JSR 289, Section 6.4.2). Thus, our work influenced the standards body to not adopt a flawed threading model. In addition, empirical studies performed in this project have contributed to the body of understanding in program comprehension and software maintenance. To our knowledge, our work is the first to explore the effects of concurrency on these key software-development activities. Finally, our work on the use of finite-state verification to assist in the design and evaluation of user studies involving computing processes and artifacts (i.e., development methods and notations) and our development of on-line tutorials to assist in training participants prior to such studies contributes to helping make these studies more objective and to prevent erroneous or ambiguous materials from being used in these very expensive studies. This may, in the long term, help the field to reduce the effort required to run these studies and thus help bring about a greater body of empirical knowledge in software engineering.
