Greif formal specification language(ID:7380/gre006)


References:
  • Greif, I. Semantics of communicating parallel processes. Proj. MAC TR-154, M.I.T., Cambridge, Mass., 1975 view details Abstract: The thesis of this dissertation is that an understanding of the ordering constraints that are introduced among events of parallel process is essential to the understanding of synchronization and that therefore any language for specifying synchronization of parallel process should be based on a theory of such orderings. While it is possible to write specifications for systems of communicating parallel processes by reference to the time ordering of some global clock external to the system, such specifications cannot be as useful as ones which are in terms of orderings derivable within the system. Specifications should place constraints on intended behavior of the computer system itself rather than on the possible observations of the system''s behaviors from some global viewpoint which may in fact be totally unrealizable. The dissertation is a development of a specification language. It is based on a model of computation in which an individual process is represented by a totally ordered set of events. Synchronization properties of systems of independent processes are guarantees that in fact the set of events in the system can be ordered by a partial order which properly contains the union of the processes'' total orders. This system ordering can be caused by the presence in a system of side-effect primitives or of synchronization primitives. Thus this model applies equally well both to busy waiting synchronization based on coordinated use of storage cells by independent processes and to non-busy waiting synchronization such as that induced by semaphores and structured synchronization primitives. In addition to applying to a range of types of synchronization, the specification language is also used to define a programming language. The meaning of a program is the specification of the behavior of the system into which that program is compiled. Specifications can be written for synchronization problems and for their implementations in terms of various primitives.
  • Greif, I. Formal problem specifications for readers and writers scheduling. Proc. MRI Symp. on Software Eng., Polytechnic Inst. of New York, 1976. view details
  • Greif, Irene "A language for formal problem specification" view details Abstract: A language for specifying the intended behavior of communicating parallel processes is described. The specifications are constraints on the order in which events of a computation can occur. The language is used to write specifications of the readers/writers problem and the writer priority of the second readers/writers problem. DOI Extract: Introduction
    Introduction
    A proof of the "correctness" of a program requires formal statements of properties of programs, proof rules for connecting those statements with the program, and informal arguments that the formal properties do indeed express intuitive notions of programmer intentions. That the formal properties represent the informal intentions can only be informally argued (see [12]). Research on formal specifications is meant to minimize this gap in formality by providing sufficiently powerful formal notations to encompass informal notions.
    Synchronization of parallel processes is an example of a problem domain which for several reasons remains difficult to formalize. One reason is the confusion between timing characteristics apparent even in abstract parallel processing and timing characteristics dependent on the run time of the properties of actual computer configurations. Thus there is a need to be precise about those timing properties which can be abstracted from run-time situations and considered program properties. Among these properties are absence of deadlock and absence of lockout (or fairness) in a synchronizer.
    In [4] we developed a language in which parallel processes can be described in terms of partial orders. In this paper we define this language in a form in which events are abstract objects to which properties such as "this is a read operation" can be attached. Thus the mapping to intuition depends on agreement on those properties, while the partial order specifications are precise.
          in [ACM] CACM 20(12) December 1977 view details
  • Cousot, P. review of Grief 1977 view details Abstract: It is argued by means of simple examples that the synchronization and priority policy of systems of communicating parallel processes can be specified by constraints on the orders in which the basic operations or sequences of operations can be executed, i.e., in which events of computations can occur. The purpose of an event of a computation (or sequence of events) or its relationship to other events is first defined by informally specified predicates. Next, a simple formal language is used to express the possible partial orderings of these events (or sequences of events) during execution.

    Several examples of specification of typical parallel program properties are exhibited, including mutual exclusion problems, first-come-first-served scheduling, absence of deadlock, readerswriters protection problem, and the writer priority of the second readers-writers problem.

    Finally, the specification of the intended behavior of parallel processes by partial orders on events is compared with the formalisms of path-expressions and event-expressions.

    Besides its use for formal specifications, the illustration of the usefulness of the formal language for program correctness proofs would have been appreciated.
          in ACM Computing Reviews 19(12) December 1978 view details