Other people have told me they'd like to do this kind of thing, but no
one has ever told me that they did it.
If you have no trouble modeling your algorithm executed under the
x86_64 memory model without instruction reordering, then that memory
model is much more understandable than the two other memory models
I've studied: Alpha and Itanium. Here's an idea for how youu might
handle instruction reordering. Suppose your code is
a: ... ;
b: ... ;
c: ... ;
d: ... ;
and A, B, C, D are the TLA+ actions that describe the effect on the
program state performed by those four atomic statements. To allow
statements b and c to be performed in either order, you can add a
variable pc to represent the control state and write the following
next-state relation
\/ /\ pc = ...
/\ pc' = {"a"}
/\ A
\/ /\ ("a" \in pc) /\ ("b" \notin pc)
/\ pc' = pc \cup {"b"}
/\ B
\/ /\ ("a" \in pc) /\ ("c" \notin pc)
/\ pc' = pc \cup {"c"}
/\ C
\/ /\ pc = {"a", "b", "c"}
/\ pc' = {"d"}
/\ D
Allowing more possible reorderings requires more complicated values of
pc and more complicated preconditions on the actions, but the idea
should work in general. If reordering is allowed between executions
of instructions in different iterations of a loop, the values of pc
will probably have to include iteration numbers of when certain
instructions were last executed, which could get pretty messy.
Leslie