Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/12572
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Dongol, B | - |
dc.contributor.author | Hierons, R | - |
dc.date.accessioned | 2016-04-25T10:03:52Z | - |
dc.date.available | 2016-04-25T10:03:52Z | - |
dc.date.issued | 2016 | - |
dc.identifier.citation | Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), New York City, USA, (5 - 8 July 2016) | en_US |
dc.identifier.uri | http://lics.rwth-aachen.de/lics16/accepted.html | - |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/12572 | - |
dc.description.abstract | Quiescent consistency is a notion of correctness for a concurrent object that gives meaning to the object's behaviours in quiescent states, i.e., states in which none of the object's operations are being executed. The condition enables greater flexibility in object design by allowing more behaviours to be admitted, which in turn allows the algorithms implementing quiescent consistent objects to be more efficient (when executed in a multithreaded environment). Quiescent consistency of an implementation object is defined in terms of a corresponding abstract specification. This gives rise to two important verification questions: \emph{membership} (checking whether a behaviour of the implementation is allowed by the specification) and \emph{correctness} (checking whether all behaviours of the implementation are allowed by the specification). In this paper, we consider the membership and correctness conditions for quiescent consistency, as well as a restricted form that assumes an upper limit on the number of events between two quiescent states. We show that the membership problem for unrestricted quiescent consistency is NP-complete and that the correctness problem is decidable, coNEXPTIME-hard, and in EXPSPACE. For the restricted form, while correctness is PSPACE-complete. | en_US |
dc.description.sponsorship | This work was funded by a Brunel University SEED grant and EPSRC grant EP/N016661/1. | en_US |
dc.language.iso | en | en_US |
dc.publisher | ACM | en_US |
dc.source | 31st ACM/IEEE Symposium on Logic in Computer Science (LICS 2016) | - |
dc.source | 31st ACM/IEEE Symposium on Logic in Computer Science (LICS 2016) | - |
dc.subject | Quiescent consistency | en_US |
dc.subject | Concurrent objects | en_US |
dc.subject | Decidability | en_US |
dc.subject | Mazurkiewicz Trace Theory | en_US |
dc.title | Decidability and complexity for quiescent consistency | en_US |
dc.type | Conference Paper | en_US |
pubs.finish-date | 2016-07-08 | - |
pubs.finish-date | 2016-07-08 | - |
pubs.publication-status | Accepted | - |
pubs.start-date | 2016-07-05 | - |
pubs.start-date | 2016-07-05 | - |
Appears in Collections: | Dept of Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 340.64 kB | Unknown | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.