DC Field | Value | Language |
---|---|---|
dc.contributor.author | Dinsdale-Young, Thomas | ko |
dc.contributor.author | Birkedal, Lars | ko |
dc.contributor.author | Gardner, Philippa | ko |
dc.contributor.author | Parkinson, Matthew | ko |
dc.contributor.author | Yang, Hongseok | ko |
dc.date.accessioned | 2017-08-08T06:54:17Z | - |
dc.date.available | 2017-08-08T06:54:17Z | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.issued | 2013-01 | - |
dc.identifier.citation | ACM SIGPLAN NOTICES, v.48, no.1, pp.287 - 299 | - |
dc.identifier.issn | 0362-1340 | - |
dc.identifier.uri | http://hdl.handle.net/10203/225276 | - |
dc.description.abstract | Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables. In this paper, we present the "Concurrent Views Framework", a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics. | - |
dc.language | English | - |
dc.publisher | ASSOC COMPUTING MACHINERY | - |
dc.title | Views: Compositional Reasoning for Concurrent Programs | - |
dc.type | Article | - |
dc.identifier.wosid | 000318629900025 | - |
dc.identifier.scopusid | 2-s2.0-84877918941 | - |
dc.type.rims | ART | - |
dc.citation.volume | 48 | - |
dc.citation.issue | 1 | - |
dc.citation.beginningpage | 287 | - |
dc.citation.endingpage | 299 | - |
dc.citation.publicationname | ACM SIGPLAN NOTICES | - |
dc.identifier.doi | 10.1145/2480359.2429104 | - |
dc.contributor.localauthor | Yang, Hongseok | - |
dc.contributor.nonIdAuthor | Dinsdale-Young, Thomas | - |
dc.contributor.nonIdAuthor | Birkedal, Lars | - |
dc.contributor.nonIdAuthor | Gardner, Philippa | - |
dc.contributor.nonIdAuthor | Parkinson, Matthew | - |
dc.description.isOpenAccess | N | - |
dc.type.journalArticle | Article | - |
dc.subject.keywordAuthor | Theory | - |
dc.subject.keywordAuthor | Verification | - |
dc.subject.keywordAuthor | concurrency | - |
dc.subject.keywordAuthor | axiomatic semantics | - |
dc.subject.keywordAuthor | compositional reasoning | - |
dc.subject.keywordPlus | SEPARATION LOGIC | - |
dc.subject.keywordPlus | LANGUAGE | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.