2013年9月1日
A fully abstract game semantics for parallelism with non-blocking synchronization on shared variables
Leibniz International Proceedings in Informatics, LIPIcs
- 巻
- 23
- 号
- 開始ページ
- 578
- 終了ページ
- 596
- 記述言語
- 英語
- 掲載種別
- 研究論文(国際会議プロシーディングス)
- DOI
- 10.4230/LIPIcs.CSL.2013.578
- 出版者・発行元
- Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
We present a fully abstract game semantics for an Algol-like parallel language with non-blocking synchronization primitive. Elaborating on Harmer's game model for nondeterminism, we develop a game framework appropriate for modeling parallelism. The game is a sophistication of the waitnotify game proposed in a previous work, which makes the signals for thread scheduling explicit with a certain set of extra moves. The extra moves induce a Kleisli category of games, on which we develop a game semantics of the Algol-like parallel language and establish the full abstraction result with a significant use of the non-blocking synchronization operation.
- ID情報
-
- DOI : 10.4230/LIPIcs.CSL.2013.578
- ISSN : 1868-8969
- SCOPUS ID : 84907500371