{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T19:45:32Z","timestamp":1725479132611},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Concurrent algorithms classically relied on locks to guarantee the absence of interference when accessing shared resources. The massive use of distributed systems and of new multi-core architectures makes this approach unfeasible, and novel techniques are needed. Lock-Free algorithms have thus gained momentum. We define a core imperative calculus, equipped with concurrency and low level lock-free synchronization primitives, based on the Load-Link\/Store-Conditional model. We propose a Hoare-Separation-style system to prove correct lock-free algorithms implemented in this language. Judgements distinguish local from global state, transfering knowledge between the worlds in the rules for loading and copying variables. We present a simple yet illustrative example of a proof for a concurrent data structure.<\/jats:p>","DOI":"10.29007\/n3nk","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T21:38:50Z","timestamp":1516743530000},"page":"1--3","source":"Crossref","is-referenced-by-count":0,"title":["A simple proof system for lock-free concurrency"],"prefix":"10.29007","volume":"12","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[]},{"given":"Carla","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"PSPL 2010. International Workshop on Proof Systems for Program Logics"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T21:38:51Z","timestamp":1516743531000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/xJD"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/n3nk","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}