Technical Report CS0628

TR#:CS0628
Class:CS
Title: DEFINING CONDITIONAL INDEPENDENCE USING COLLAPSES
Authors: Shmuel Ka~z and Doron Pe1ed
PDFCS0628.pdf
Abstract: Trace semantics is extended to allow conditional commutativity among operations. Conditional commutativity is obtained by identifying the context (the set of global states) in which operations are commutative using special predicates. These will allow collapsing execution histories into equivalence classes of conditional traces. Using this approach, it i possible that the execution of two operations will be dependent in one context and independent in another. The predicates allow defining a family of possible semantic definitions for each language, where each is an extension of previous standard definitions. Examples are shown when such a semantics is desired. As an example of an application, a proof method for total correctness is introduced.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1990/CS/CS0628), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1990
To the main CS technical reports page

Computer science department, Technion
admin