uu.seUppsala universitets publikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Context-Bounded Analysis of TSO Systems
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
LIAFA, CNRS and University of Paris Diderot. (Modeling and Verification)
University of Southampton.
2014 (Engelska)Ingår i: From Programs to Systems: The Systems perspective in Computing / [ed] Bensalem, S; Lakhneck, Y; Legay, A, Springer, 2014, s. 21-38Konferensbidrag, Publicerat paper (Övrigt vetenskapligt)
Abstract [en]

We address the state reachability problem in concurrent programs running over the TSO weak memory model. This problem has been shown to be decidable with non-primitive recursive complexity in the case of finite-state threads. For recursive threads this problem is undecidable. The aim of this paper is to provide under-approximate analyses for TSO systems that are decidable and have better (elementary) complexity. We propose three bounding concepts for TSO behaviors that are inspired from the concept of bounding the number of context switches introduced by Qadeer and Rehof for the sequentially consistent (SC) model. We investigate the decidability and the complexity of the state reachability problems under these three bounding concepts for TSO, and provide reduction of these problems to known reachability problems of concurrent systems under the SC semantics.

Ort, förlag, år, upplaga, sidor
Springer, 2014. s. 21-38
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8415
Nyckelord [en]
weak memory models, under-approximation techniques
Nationell ämneskategori
Datorsystem
Forskningsämne
Datavetenskap
Identifikatorer
URN: urn:nbn:se:uu:diva-238133DOI: 10.1007/978-3-642-54848-2ISI: 000348370400002ISBN: 978-3-642-54847-5 (tryckt)ISBN: 978-3-642-54848-2 (tryckt)OAI: oai:DiVA.org:uu-238133DiVA, id: diva2:770097
Konferens
Workshop on From Programs to Systems - The Systems Perspective in Computing (FPS) held in Honor of Joseph Sifakis, April 6, 2014, Grenoble, France
Projekt
UPMARCWeak Memory ModelsTillgänglig från: 2014-12-09 Skapad: 2014-12-09 Senast uppdaterad: 2015-03-11Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Personposter BETA

Atig, Mohamed Faouzi

Sök vidare i DiVA

Av författaren/redaktören
Atig, Mohamed Faouzi
Av organisationen
Datorteknik
Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 586 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf