Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Temporal Logic Framework for Performance Analysis of Architectures of Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Semantics for Locking Specifications

verfasst von : Michael D. Ernst, Damiano Macedonio, Massimo Merro, Fausto Spoto

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Lock-based synchronization disciplines, like Java’s @GuardedBy, are widely used to prevent concurrency errors. However, their semantics is often expressed informally and is consequently ambiguous. This article highlights such ambiguities and overcomes them by formalizing two possible semantics of @GuardedBy, using a reference operational semantics for a core calculus of a concurrent Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound tools that verify or infer them.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Hierarchical Verification of Quantum Circuits
Nächstes Kapitel From Design Contracts to Component Requirements Verification
Literatur
1.
Abadi, M., Flanagan, C., Freund, S.: Types for safe locking: static race detection for Java. ACM TOPLAS 28(2), 207–255 (2006)CrossRef
2.
Ábrahám-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 5–20. Springer, Heidelberg (2002)CrossRef
3.
4.
Bierman, G.M., Parkinson, M.J.: Effects and effect inference for a core java calculus. ENTCS 82(7), 82–107 (2003)
5.
Blanchet, B.: Escape analysis for java: theory and practice. ACM TOPLAS 25(6), 713–775 (2003)CrossRef
6.
Bogdanas, D., Rosu, G.: K-java: a complete semantics of java. In: ACM SIGPLAN-SIGACT POPL, pp. 445–456, Mumbai, India (2015)
7.
Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: From sequential to multi-threaded java: an event-based operational semantics. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 75–90. Springer, Heidelberg (1997)CrossRef
8.
Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Taylor, R.N., Gall, H.C. (eds.) ICSE 2011 (2011)
9.
Ernst, M.D., Macedonio, D., Merro, M., Spoto, F.: Semantics for locking specifications. CoRR abs/1501.05338 (2015)
10.
Ernst, M., Lovato, A., Macedonio, D., Spoto, F., Thaine, J.: Locking discipline inference and checking. In: ICSE 2016, Austin, TX, USA (2016)
11.
Goetz, B., Peierls, T., Bloch, J., Bowbeer, J.: Java Concurrency in Practice. Addison Wesley, Boston (2006)
12.
13.
Hatcliff, J., Dwyer, M.B.: Using the bandera tool set to model-check properties of concurrent java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 39. Springer, Heidelberg (2001)CrossRef
14.
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight java: a minimal core calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)CrossRef
15.
16.
17.
Long, B., Long, B.W.: Formal specification of java concurrency to assist software verification. In: Dongarra, J. (ed.) IPDPS 2003. IEEE Computer Society (2003)
18.
19.
Nikolić, D.J., Spoto, F.: Definite expression aliasing analysis for java bytecode. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 74–89. Springer, Heidelberg (2012)CrossRef
20.
Östlund, J., Wrigstad, T.: Welterweight java. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 97–116. Springer, Heidelberg (2010)CrossRef
21.
Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Paepcke, A. (ed.) OOPSLA 1991, pp. 146–161. ACM SIGPLAN Notices, ACM, New York (1991)
22.
Metadaten
Titel
Semantics for Locking Specifications
verfasst von
Michael D. Ernst
Damiano Macedonio
Massimo Merro
Fausto Spoto
Copyright-Jahr
2016
Buch
NASA Formal Methods

Print ISBN: 978-3-319-40647-3

Electronic ISBN: 978-3-319-40648-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40648-0_27