English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present an extensional semantics for parallel programs based on predicate transformers. We identify the meaning of a parallel program with three concepts: a set of initial conditions, a predicate transformer, called wlt, characterizing progress properties of the program, and a predicate transformer wsafe concerned with safety aspects. For a given program, these predicate transformers are defined in terms of fixpoints of recursive equations. The basis for our semantics are two completeness results: the first one states that the fixpoint characterization of wlt completely captures the notion of progress under weak fairness, with programs modelled as infinite directed computation trees. Similarly, the second completeness theorem relates wsafe and safety prop erties. In addition, we show that Chandy and Misra’s theory of UNITY has the same expressive power as our approach. We apply the results obtained to derive new, shorter and more direct proofs of a number of UNITY theorems and prove that for UNITY, wlt does not enjoy a number of junctivity properties such as or-continuity. Finally, we draw some connections to Temporal Logics of programs. *Supported in part by NSF-CCR-851-1354 tsupported in part by ONR contract N00014-87-K-0510 Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

A predicate transformer approach to semantics of parallel programs