Hide metadata

dc.date.accessioned2018-06-28T14:45:31Z
dc.date.available2018-06-28T14:45:31Z
dc.date.created2018-01-31T11:34:30Z
dc.date.issued2018
dc.identifier.urihttp://hdl.handle.net/10852/61977
dc.description.abstractA multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, they must be lax enough to allow for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to reason about programs. Though the right balance is up for debate, a memory model should provide what is known as the SC-DRF guarantee, meaning that data-race free programs behave in a sequentially consistent manner. In this work we present a weak memory model for a calculus inspired by Go. Thus, different from previous approaches, we focus on a memory model with buffered channel communication as the sole synchronization primitive. While memory models are often defined axiomatically where the notion of a program is abstracted away (often as a graph with memory events as nodes), we formalize our model via an operational semantics. This allows us to prove the SC-DRF guarantee using a standard simulation technique that highlights invariants and gives insight into the how the memory works. Finally, we provide a concrete implementation in K, a rewrite-based executable semantic framework, which allows us to derive an interpreter for the proposed language.
dc.languageEN
dc.publisherUniversitetet i Oslo
dc.relation.ispartofResearch report http://urn.nb.no/URN:NBN:no-35645
dc.relation.urihttp://urn.nb.no/URN:NBN:no-35645
dc.titleOperational Semantics of a Weak Memory Model with Channel Synchronization
dc.typeResearch report
dc.creator.authorFava, Daniel Schnetzer
dc.creator.authorSteffen, Martin
dc.creator.authorStolz, Volker
cristin.unitcode185,15,5,32
cristin.unitnameForskningsgruppen for presis modellering og analyse
cristin.ispublishedtrue
cristin.fulltextoriginal
dc.identifier.cristin1558119
dc.identifier.pagecount40
dc.identifier.urnURN:NBN:no-64575
dc.type.documentForskningsrapport
dc.source.isbn978-82-7368-442-4
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/61977/1/fava2018operational.pdf


Files in this item

Appears in the following Collection

Hide metadata