On verifying TSO robustness for event-driven asynchronous programs

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We present a method for checking whether an event-driven asynchronous program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. We show that this verification problem can be reduced in polynomial time to a reachability problem in a program with two threads, provided that the original program satisfies a criterion called robustness against concurrency, introduced recently in the literature. This result allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity.

Original languageEnglish
Title of host publicationNetworked Systems - 6th International Conference, NETYS 2018, Revised Selected Papers
EditorsAndreas Podelski, François Taïani
PublisherSpringer Verlag
Pages225-239
Number of pages15
ISBN (Print)9783030055288
DOIs
Publication statusPublished - 1 Jan 2019
Externally publishedYes
Event6th International Conference on Networked Systems, NETYS 2018 - Essaouira, Morocco
Duration: 9 May 201811 May 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11028 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Conference on Networked Systems, NETYS 2018
Country/TerritoryMorocco
CityEssaouira
Period9/05/1811/05/18

Fingerprint

Dive into the research topics of 'On verifying TSO robustness for event-driven asynchronous programs'. Together they form a unique fingerprint.

Cite this