As apparent from herd output, there are four execution candidates:
% herd7 -cat empty.cat R.litmus Test R Allowed States 4 1:X3=0; [y]=1; 1:X3=0; [y]=2; 1:X3=1; [y]=1; 1:X3=1; [y]=2; Ok Witnesses Positive: 1 Negative: 3 Condition exists ([y]=2 /\ 1:X3=0) Observation R Sometimes 1 3 Time R 0.01 Hash=78c40b6f8d16b9e5ea74321e4bfc1c40
Both the count of witnesses Positive: 1 Negative: 3 and the
observation summary Observation R Sometimes 1 3 suffices to
compute the number of executions.
It is also possible to display the executions:
% herd7 -conf show.cfg -cat empty.cat -show all -gv R.litmus
The command above produces four images, one per execution.
We now clearly see that the four executions results from two possible
choices of rf for the read of x “d” combined with two
possible choices for ordering the writes to y “b” and “c”.