Rosenblum, D.; (1988) Design and verification of distributed tasking supervisors for concurrent programming languages. Doctoral thesis , Stanford University.

Preview

PDF 6.4_dissertation.pdf Download (997kB)

Abstract

A tasking supervisor implements the concurrency constructs of a concurrent programming language. This thesis addresses two fundamental issues in constructing distributed implementations of a concurrent language: (1) Principles for designing a tasking supervisor for the language, and (2) Practical techniques for verifying that the supervisor correctly implements the semantics of the language. Previous research in concurrent languages has focused on the design of constructs for expressing concurrency, while ignoring these two important implementation issues. First, the thesis describes the design of a tasking supervisor for the Ada programming language. The Supervisor implements the full Ada tasking language, and it performs distributed program execution on multiple CPUs. The Supervisor is a portable, modular, distributed software system written in Ada. The interface between the Supervisor and application programs forms the topmost layer of the Supervisor and is formally specified in Anna (ANNotated Ada). All machine dependences are encapsulated in the bottom layer of the Supervisor; this layer is an implementation of an abstract virtual loosely coupled multiprocessor. The principles used to design the Supervisor may be used to design a distributed supervisor for any concurrent language. Second, the thesis presents new and practical techniques for automatically verifying the behavior of a distributed supervisor; these techniques are illustrated by the verification of the Distributed Ada Supervisor. An event-based formalization of the Ada tasking semantics is expressed as a collection of machine-processable specifications written in TSL (Task Sequencing Language). Correctness of the Supervisor is established by automatically checking executions of test programs for consistency with the TSL specifications. Since the specifications are derived solely from the Ada semantics, the specifications can be used to test any implementation of Ada tasking. In addition, every Ada tasking program may be used as test input. The theory and practice of concurrent programming is in its infancy. The research described in this thesis represents a major step toward the development of a theory of constructing multiprocessor implementations of concurrent programming languages.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as CSVJSONXML

Archive Staff Only

View Item