From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Dec 2012 23:14:29 +0000 (-0800)
Subject: model: distinguish between 'read' and 'acquire' in release sequences
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=20f8e2bc8677046c4bd7cb0bb80696ced41301f2;hp=20f8e2bc8677046c4bd7cb0bb80696ced41301f2

model: distinguish between 'read' and 'acquire' in release sequences

When using fences, we may have a fence-acquire preceded by a non-acquire
load, where the load takes part in a "hypothetical release sequence" (as
named by Mathematizing C++). So, I add a parameter to
get_release_seq_heads() and to struct release_seq so that we record the
'acquire' operation separately from the 'read'.

For our traditional release sequences, 'acquire' and 'read' will be the
same ModelAction. But fence-acquire support will utilize distinct
actions.
---