Sökning: onr:"swepub:oai:DiVA.org:uu-298663" >
The benefits of dua...
-
Abdulla, Parosh AzizUppsala universitet,Datorteknik
(författare)
The benefits of duality in verifying concurrent programs under TSO
- Artikel/kapitelEngelska2016
Förlag, utgivningsår, omfång ...
-
Dagstuhl, Germany :Leibniz-Zentrum für Informatik,2016
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:uu-298663
-
https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-298663URI
-
https://doi.org/10.4230/LIPIcs.CONCUR.2016.5DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes.In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Atig, Mohamed FaouziUppsala universitet,Datorteknik(Swepub:uu)mohat117
(författare)
-
Bouajjani, Ahmed
(författare)
-
Ngo, Tuan PhongUppsala universitet,Datorteknik(Swepub:uu)tuang296
(författare)
-
Uppsala universitetDatorteknik
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:27th International Conference on Concurrency TheoryDagstuhl, Germany : Leibniz-Zentrum für Informatik, s. 5:1-159783959770170
Internetlänk
Hitta via bibliotek
Till lärosätets databas