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

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.