What's Decidable about Causally Consistent Shared Memory?

Ori Lahav, Udi Boker

פרסום מחקרי: פרסום בכתב עתמאמרביקורת עמיתים

תקציר

While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still unclear. In this article, we establish the decidability of this problem for two standard and well-studied variants of causal consistency. To do so, for each variant, we develop an equivalent "lossy"operational semantics, whose states track possible futures, rather than more standard semantics that record the history of the execution. We show that these semantics constitute well-structured transition systems, thus enabling decidable verification. Based on a key observation, which we call the "shared-memory causality principle,"the two novel semantics may also be of independent use in the investigation of weakly consistent models and their verification. Interestingly, our results are in contrast to the undecidability of this problem under the Release/Acquire fragment of the C/C++11 memory model, which forms another variant of causally consistent memory that, in terms of allowed outcomes, lies strictly between the two models studied here. Nevertheless, we show that all these three variants coincide for write/write-race-free programs, which implies the decidability of verification for such programs under Release/Acquire.

שפה מקוריתאנגלית
מספר המאמר8
כתב עתACM Transactions on Programming Languages and Systems
כרך44
מספר גיליון2
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - יוני 2022

ASJC Scopus subject areas

  • ???subjectarea.asjc.1700.1712???

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'What's Decidable about Causally Consistent Shared Memory?'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי