Ribbon Diagrams for Weak Memory

In their POPL’17 paper, Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathy Gray, Ali Sezgin, Mark Batty, and Peter Sewell describe a semantics of weakly-consistent memory that copes (for the first time) with mixed-size memory accesses. In this blog post, I describe how their semantics can be explained rather nicely with some graphical ‘ribbon’ diagrams.

The Flur et al. semantics deals with programs that access individual bytes of memory as well as whole words (four bytes). For instance, given a program that writes a word starting at memory location {\tt x},

{\tt stw~0x03020100~0(x)}

then writes one byte starting at {\tt x}+2,

{\tt stb~0x11~2(x)}

and then reads the word starting at {\tt x},

{\tt lwz~r~0(x)}

their semantics can deduce that {\tt r} must end up holding {\tt 0x03021100}.

Like much work on weakly-consistent memory, the semantics is based on execution graphs. An execution graph is like a trace of a program, in that it comprises a set of runtime events; unlike a normal trace, the events do not occur in a simple sequence, but instead form the vertices of a mathematical graph. Relating the events are various kinds of arrow. Program order arrows capture the order in which the corresponding instructions are written in each thread of the source code; reads-from arrows show store events passing values to load events; and coherence order arrows depict the order in which stored values reach main memory.

Flur et al.’s paper uses conventional diagrams to depict these executions. For instance, the following diagram from their paper captures an execution of the program described above. Store events are labelled with a ‘W’, load events are labelled with an ‘R’, the black arrows are program order, brown arrows are coherence order (co), and red arrows are reads-from (rf).

mixed-size1

Note that some arrows are annotated with the set of memory locations that they are concerned with; for instance, the left-hand rf arrow is annotated with {\tt x}/2 and {\tt x}+3/1 to convey, respectively, that two bytes are being read starting from location {\tt x}, and that one byte is being read starting from the third byte after {\tt x}.

As such, these arrows are naturally associated with some sort of ‘thickness’. With this in mind, I propose the following alternative diagram for this execution.

mixed-size2.png

In my diagram, the reads-from relation and the coherence order are shown using red and blue ‘ribbons’ (respectively); program order is still depicted using black arrows. The position and thickness of a ribbon as it meets the rectangular outline of an event conveys which bytes the ribbon is concerned with. For instance, the load event can be seen to obtain its first two bytes from the {\tt W x/4} event, since that ribbon attaches to the first half of the load event’s top edge. The third byte comes from the {\tt W x+2/1} event, and the fourth comes from the {\tt W x/4} event. In this way, my diagram conveys the same information as Flur et al.’s original diagram, but requires much less text.

Unlike arrows, ribbons have no inherent directionality, but my diagram remains unambiguous because coherence ribbons always start at the bottom edge of a store event and end at the top edge of another store event, and because reads-from ribbons always start at the right-hand edge of a store event and end at the top edge of a load event.

Here are two further examples. The first is an execution that resembles the classic message-passing test: if one thread performs a double-word store, can another thread use two single-word loads to observe that the two words are not written simultaneously?mixed-size3.png

In my diagrammatic system, this execution would be drawn as follows.

mixed-size4.png

The last example is another execution from the message-passing family: if one thread writes to two consecutive words using two consecutive store instructions, can another thread use one double-word load to observe the two stores taking effect out-of-order? mixed-size5.png

In my diagrammatic system, this execution would be drawn as follows.

mixed-size6.png

In conclusion, I think this is quite a neat way to draw execution graphs for mixed-size concurrency. The main limitation is, of course, scalability: even for very small examples these diagrams need a lot of space, and a lot of attention must be paid to finding a good layout; this problem will surely make this diagrammatic system unmanageable for even slightly bigger examples. Still, a fun experiment!

All the LaTeX source code for making the ribbon diagrams in this post is available in my GitHub repository.

 

Advertisements

1 thought on “Ribbon Diagrams for Weak Memory”

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

w

Connecting to %s