The design and verification of a programming language for distributed processes communication [microform]
- Bib ID:
- 3287373
- Format:
- Book and Microform
- Author:
- Mao, Tsang William
- Description:
- 210 p.
- Summary:
-
This work studies the design and validation of a programming language for a distributed environment where many processors cooperate to complete a single task. The processors share no common memory and communicate with each other through hardware busses. This environment can be seen as an abstract model of many networks and microprocessor networks. We consider the design of a distributed language, DLCP, which draws most of its features from Algol-descendent languages such as Pascal. The basic components in the language are processes, which are assumed to be executed in parallel. Strong emphasis is placed on communication facilities for processes. Since no shared variables exist, communication is by message passing. To simplify the implementation of the language, we further assume that the distributed environment does not support automatic buffering of messages. Information exchange therefore must be totally synchronized.
Communication Ports (CP), influenced by Hoare's communicating sequential processes, are proposed as a generalized mechanism for both information exchange and synchronization among processes. During communication, the processes behave as if they merge into a single process. To provide greater concurrency, another feature is introduced to allow early disconnection of communication. CP also provides compiler-time message type checking and a run-time mechanism to schedule call acceptances. Many examples are given showing the equivalence of CP and the communication and synchronization features of other proposed languages. In order to formally define the semantics of DLCP, Hoare's deductive system of axioms and assertions is extended to include distributed programs. Semantic rules are developed to define the semantics of CP. We also develop proof rules which, when combined with semantic rules, can be used to prove functional correctness of distributed programs written in DLCP.
Functional correctness of multi-process programs is generally considered to be a property global to the whole program, and requires all assertions in a proof to meet a condition, called speed independence. With the aid of a state machine model about programs' execution, we show that functional correctness may be proven if only a subset of the program assertions are speed independent. The effort to discover proper assertions and invent auxiliary variables for proving a program is thus reduced. Finally, the feasibility of implementing DLCP on a processor network is assessed. An algorithm, using message send and receive as primitives, is developed to enable a process in DLCP to communicate with other processes efficiently. The run-time support system needed to interface a process with the processor it resides and other processes in other processors is discussed. A prototype of such a system, embedding the algorithm, is designed, illustrated, and coded in Concurrent Pascal.
This Concurrent Pascal program runs on a distributed system which composes of a PDP-11/60 and LSI microprocessors.
- Notes:
-
- (UnM)AAI8109200
- Source: Dissertation Abstracts International, Volume: 41-11, Section: B, page: 4185.
- Thesis (Ph.D.)--The University of Texas at Austin, 1980.
- Reproduction:
- Microfiche. Ann Arbor, Mich.: University Microfilms International.
- Subject:
- Computer Science
- Other authors/contributors:
- The University of Texas at Austin
- Copyright:
-
In Copyright
Contact us for information about copying.
Copyright status was determined using the following information:
- Material type:
- Literary Dramatic Musical
- Published status:
- Unpublished
- Creation date:
- 1980
Copyright status may not be correct if data in the record is incomplete or inaccurate. Other access conditions may also apply. For more information please see: Copyright in library collections.
Request this item
Request this item to view in the Library’s reading room.