In this chapter we have provided sketches for a semantics with delayed reads and well as delayed writes. The reduction rules in Section 5.2 lay out the ground work.
Rule R-DEREFfaithfully follows the Go memory model observability rules, which specify when a read is allowed to observe a write.
In Section 5.3, we show that there exist relaxations involving delayed reads and branches that are not accounted for in the reduction rules of Section 5.2. We ex-plore ways to further relax the operational semantics by branching on symbolic reads—this addition gives the semantics the flavor of speculative execution. The relaxation afforded by symbolic branching, however, goes too far: the augmented semantics admits out-of-thin-air behavior. We draw parallels between operational and axiomatic semantics and conclude Section 5.3 with ideas on how to potentially deal with branches. Section 5.4 introduces channels and argues for the need to send symbolic values (i.e.,read event labels) over channels.
10By sending a symbolic value, we are able to obtain a reduction like in Example 4 and the end-result of(r1,r2) = (42,42).
We point at open questions throughout the chapter. Here, we remind the reader of the importance of establishing the DRF-SC guarantee for the delayed read/write semantics. This may involve the proof in Chapter 2 as a stepping stone.
Finally, it is worth noticing that the operational semantics discussed at the end of Section 5.3 starts to have the same flavor as its axiomatic counterparts. The op-erational semantics is, in essence, collecting concrete and symbolic memory events.
These events carry information that allow us to relate them to one another; for ex-ample, they are related through their happens-before and shadow sets and through path variables. Like events of an axiomatic semantics, the memory events of the op-erational semantics can thus be interpreted as vertices that can be connected to one another. It would be interesting to further explore the parallels between operational and axiomatic semantics, and to seek a correspondence between the two approaches.
6
Conclusion and extensions
Each society and each individual usually explore only a tiny fraction of the horizon of possibilities.
Yuval Noah Harari,Sapiens In the introduction, we set three goals for this thesis. The first was topropose and evaluate a memory model for message passing systems using an operational semantics as formalism. In Chapter 2, we presented a memory model inspired by the Go programming language, where threads synchronize by exchanging messages over channels. In that chapter, we also addressed the goal of investigating how relaxed the model can be while keeping out-of-thin-air behavior at bay and while supporting the DRF-SC guarantee—which says that Data-Race Free executions are Sequentially Consistent. This second goal was addressed by showing the absence of out-of-thin-air (OOTA) behavior and by proving the DRF-SC guarantee for a memory model supporting delayed writes.
The formalisms introduced in Chapter 2 can, however, be generalized by in-corporating delayed reads (aka. load buffering). The further relaxation associated with delayed reads, however, presents significant challenges with respect to non-termination and the introduction of OOTA behavior. These challenges require fur-ther investigation, as discussed in Chapter 5.
In Chapter 3, we explored data-race detection and showed, in Chapter 4, how our formalisms helped unveil and remedy a bug in the Go runtime. These chapters support our third goal ofrelating the theoretical model to its “material” counterpart and source of inspiration: the Go programming language.
Here, we discuss additional extensions of our work, such as the potential for improvements in data-race detection, the verification of Go programs via model checking, and the exploration of language constructs at the intersection of concur-rency and distribution.
6.1 Data-race detection
Even though Go is a language with channels, the infrastructure underlying the Go data-race detector is based on lock semantics! Locks have been the prevalent mode of synchronization partially because they can easily be mapped down to hardware, but employing locks are not always the best approach. As part of this thesis, we introduced a primitive (therelease-acquire-exchangeof Chapter 4) that closely matches the semantics of channels into the underlying data-race detector used in Go. By doing so, we not only repaired the detector’s functionality but also
133
improved its performance and memory consumption—see Section 4.5. We would like to see further improvements.
One a practical side, the underlying race detector employed by Go is written in C/C++and reside in a different repository than the language itself. This complicates the process of upgrading the detector and keeping it in sync with the language. Al-though powerful, the detector is overly complex: it was originally built for detecting races in C++11, which means that large portions of the code base do not apply to Go.
This added complexity creates a high barrier of entrance when it comes to modifying and improving the detector.
Go is a language for systems design and is thus suited for implementing a data-race detector. An implementation in Go, for Go, is not just an exercise of the “eat your own dog food” principle [103]. More importantly, a tailor-made implementa-tion would be simpler and thus easier to modify and extend than the existing detec-tor’s code base. This simplicity would likely translate to improvements and to new features for the end user. We are particularly interested in exploiting the concept of stale vector-clock entries, defined in Chapter 3, Section 3.5.1. We conjecture that the memory consumption associated with a vector-clock based data-race detector can be reduced by taking the concept of stale entries into account.