Title :
Full abstraction for a shared variable parallel language
Author :
Brookes, Stephen
Author_Institution :
Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
Abstract :
Gives a new denotational semantics for a shared variable parallel programming language and proves full abstraction. The semantics gives identical meanings to commands if and only if they induce the same partial correctness behavior in all program contexts. The meaning of a command is a set of transition traces, which record the ways in which a command may interact with and be affected by its environment. It is shown how to modify the semantics to incorporate new program constructs, to allow for different levels of granularity or atomicity, and to model fair infinite computation, in each case achieving full abstraction with respect to an appropriate notion of program behavior
Keywords :
parallel languages; parallel programming; programming theory; atomicity; denotational semantics; fair infinite computation; full abstraction; granularity; identical command meanings; partial correctness behavior; program behavior; program constructs; program contexts; shared variable parallel programming language; transition traces; Aerospace electronics; Computer science; Context modeling; Contracts; Equations; Government; Parallel languages; Reasoning about programs; Research and development; System recovery;
Conference_Titel :
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-3140-6
DOI :
10.1109/LICS.1993.287596