Skip to main content

2013 | OriginalPaper | Buchkapitel

SPIN as a Linearizability Checker under Weak Memory Models

verfasst von : Oleg Travkin, Annika Mütze, Heike Wehrheim

Erschienen in: Hardware and Software: Verification and Testing

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Linearizability is the key correctness criterion for concurrent data structures like stacks, queues or sets. Consequently, much effort has been spent on developing techniques for showing linearizability. However, most of these approaches assume a sequentially consistent memory model whereas today’s multicore processors provide relaxed out-of-order execution semantics.

In this paper, we present a new approach for checking linearizability of concurrent algorithms under weak memory models, in particular the TSO memory model. Our technique first compiles the algorithm into intermediate low-level code. For achieving the out-of-order execution, we (abstractly) model the processor’s architecture with shared memory and local buffers. Low-level code as well as architecture model are given as input to the model checker SPIN which checks whether the out-of-order execution of the particular algorithm is linearizable. We report on experiments with different algorithms.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Metadaten
Titel
SPIN as a Linearizability Checker under Weak Memory Models
verfasst von
Oleg Travkin
Annika Mütze
Heike Wehrheim
Copyright-Jahr
2013
Verlag
Springer International Publishing
DOI
https://doi.org/10.1007/978-3-319-03077-7_21