Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

On Atomicity in Presence of Non-atomic Writes

Authors : Constantin Enea, Azadeh Farzan

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The inherently nondeterministic semantics of concurrent programs is the root of many programming errors. Atomicity (more precisely conflict serializability) has been used to reduce the magnitude of this nondeterminism and therefore make it easier to understand the behaviour of the concurrent program. Serializability, however, has not been studied well for programs executed under memory models weaker than sequential consistency (SC), where writes are not atomic, i.e., they may be committed to the main memory later than issued. In this paper, we define the notion of conflict serializability for the Total Store Ordering (TSO) memory model, and study the relation between TSO-serializability and the well-known notions of SC-serializability and robustness. We investigate the algorithmic problem of monitoring program executions for violations of serializability, and provide lower bound complexity results for the problem, and new algorithms to perform the monitoring efficiently.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Approaching the Coverability Problem Continuously
next chapter Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
Footnotes
1
Transaction-fenced programs are not necessarily robust since statements inside a transaction may not be followed by a fence.
 
Literature
1.
2.
Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50–66. Springer, Heidelberg (2011)CrossRef
3.
Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 428–440. Springer, Heidelberg (2011)CrossRef
4.
Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013)CrossRef
5.
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290–309. Springer, Heidelberg (2013)CrossRef
6.
Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008)CrossRef
7.
Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012)CrossRef
8.
Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11–25. Springer, Heidelberg (2011)CrossRef
9.
Dice, D., Lev, Y., Moir, M., Nussbaum, D.: Early experience with a commercial hardware transactional memory implementation. In: ASPLOS 2009, pp. 157–168 (2009)
10.
Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52–65. Springer, Heidelberg (2008)CrossRef
11.
Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 155–169. Springer, Heidelberg (2009)CrossRef
12.
Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89–109 (2008)MathSciNetCrossRefMATH
13.
Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: static checking and inference for java. ACM Trans. Program. Lang. Syst. 30(4), 20 (2008)CrossRef
14.
Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: PLDI 2008, pp. 293–303 (2008)
15.
Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Heidelberg (2012)CrossRef
16.
Harris, T.L., Fraser, K.: Language support for lightweight transactions. In: OOPSLA 2003, pp. 388–402 (2003)
17.
Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 175–190. Springer, Heidelberg (2004)CrossRef
18.
Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: ISCA 1993, pp. 289–300 (1993)
19.
Jagadeesan, R., Petri, G., Pitcher, C., Riely, J.: Quarantining weakness. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 492–511. Springer, Heidelberg (2013)CrossRef
20.
Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS, pp. 329–339 (2008)
21.
22.
Shavit, N., Touitou, D.: Software transactional memory. Distrib. Comput. 10(2), 99–116 (1997)CrossRef
23.
Sinha, A., Malik, S., Wang, C., Gupta, A.: Predicting serializability violations: SMT-based search vs. DPOR-based search. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 95–114. Springer, Heidelberg (2012)CrossRef
24.
von Praun, C., Gross, T.R.: Static detection of atomicity violations in object-oriented programs. J. Object Technol. 3(6), 103–122 (2004)CrossRef
25.
Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng. 32(2), 93–110 (2006)CrossRef
26.
Yi, J., Disney, T., Freund, S.N., Flanagan, C.: Cooperative types for controlling thread interference in java. In: ISSTA 2012, pp. 232–242 (2012)
Metadata
Title
On Atomicity in Presence of Non-atomic Writes
Authors
Constantin Enea
Azadeh Farzan
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_29

Premium Partner

    Image Credits