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:
Multi-purpose Syntax Definition with SDF3 Kapitel lesen Erstes Kapitel lesen

2020 | OriginalPaper | Buchkapitel

Finding and Fixing a Mismatch Between the Go Memory Model and Data-Race Detector

A Story on Applied Formal Methods

verfasst von : Daniel Schnetzer Fava

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Go is an open-source programming language developed at Google. In previous works, we presented formalizations for a weak memory model and a data-race detector inspired by the Go specification. In this paper, we describe how our theoretical research guided us in the process of finding and fixing a concrete bug in the language. Specifically, we discovered and fixed a discrepancy between the Go memory model and the Go data-race detector implementation—the discrepancy led to the under-reporting of data races in Go programs. Here, we share our experience applying formal methods on software that powers infrastructure used by millions of people.

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 Multi-purpose Syntax Definition with SDF3
Nächstes Kapitel Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
There are good reasons why a type checker cannot enforce such a discipline without seriously restricting the language.
 
2
The relation below can be derived by both program-order as well as by rule (I). Similar for the send and receive operations performed by T1.
$$\begin{aligned} c \leftarrow 0~\text {by}~T0 ~~\sqsubset _{hb}~~ \mathop {\leftarrow c}{}~\text {by}~T0 \end{aligned}$$
.
 
3
In the implementation of the send operation, a message is moved from the sender’s buffer to a receiver’s buffer ep on line 16. The index c.sendx is incremented in line 19 and the increment wraps around based on the length of the array—lines 20 to 22. The number of elements in the array is incremented, the lock protecting the channel is unlocked and the function returns—lines 23 to 25.
 
4
The send operation by T0 is analogous to acquire and the receive to release.
 
5
Recall that the mutual exclusion and message passing patterns were introduced in Fig. 1 and discussed in Sect. 2.
 
7
The place-holder is a variable local to a function in TSan, as opposed to an extra memory region allocated in Go.
 
9
As noted in [5], “the interplay between forward and backward channels can also be understood as a form of flow control. Entries in the backward channel’s queue are not values deposited by threads. Instead, [these entries] can be seen as tickets that grant senders a free slot in the communication channel.”.
 
12
For example, the closing of channels in both  [4] and in Go cause happens-before information to be deposited onto the channel, regardless of whether the channel is full.
 
13
Our observation about the representational different between specification and implementation is not new. The idea of bridging specification and implementation has been tackled by many fronts, for example  [1].
 
14
Because of stigma, the “formal” qualifier has been de-emphasized when disseminating formal methods in industry  [13]. This stance has shifted dramatically  [3].
 
16
Because of differences in how vector clocks are allocated and managed, the memory gains reported by the reference data-race detector may be different from TSan’s.
 
Literatur
1.
2.
Brewer, E.A.: Kubernetes and the path to cloud native. In: Ghandeharizadeh, S., Barahmand, S., Balazinska, M., Freedman, M.J. (eds.) Proceedings of the Sixth ACM Symposium on Cloud Computing, SoCC 2015, Kohala Coast, Hawaii, USA, August 27–29, 2015, p. 167. ACM (2015)
3.
4.
Fava, D., Steffen, M., Stolz, V.: Operational semantics of a weak memory model with channel synchronization. J. Log. Algebr. Methods Program. 103, 1–30 (2019). An extended version of the FM 18 publication with the same titleMathSciNetCrossRef
5.
Fava, D.S., Steffen, M.: Ready, set, Go! data-race detection and the Go language. Sci. Comput. Program. 195, 102473 (2020)CrossRef
6.
7.
8.
9.
10.
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRef
11.
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, 2004, CGO 2004, pp. 75–86. IEEE (2004)
12.
Merkel, D.: Docker: lightweight Linux containers for consistent development and deployment. Linux J. 2014(239), 2 (2014)
13.
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)CrossRef
Metadaten
Titel
Finding and Fixing a Mismatch Between the Go Memory Model and Data-Race Detector
verfasst von
Daniel Schnetzer Fava
Copyright-Jahr
2020
Buch
Software Engineering and Formal Methods

Print ISBN: 978-3-030-58767-3

Electronic ISBN: 978-3-030-58768-0

Copyright-Jahr: 2020

DOI
https://doi.org/10.1007/978-3-030-58768-0_2