Next: Result of supercompilation
Up: Firefly
Previous: Firefly
* DEC firefly cache coherence protocol
*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;
$ENTRY Go {e.A (e.i) = <Loop (e.A) (Invalid e.i)(Dirty )(Shared )(Exclusive ) >;}
Loop {
() (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
<Result (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>;
(s.A e.A) (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
<Loop (e.A)
<RandomAction s.A
(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>>;
}
RandomAction {
* rh Trivial
* rm_1
A (Invalid s.1 e.1) (Dirty ) (Shared ) (Exclusive )
=(Invalid e.1) (Dirty ) (Shared ) (Exclusive s.1);
*
*rm_2
B (Invalid s.1 e.1)(Dirty s.2 e.2)(Shared e.3)(Exclusive e.4) =
(Invalid e.1)(Dirty e.2)(Shared s.1 s.2 e.3)(Exclusive e.4);
* rm_3
C (Invalid s.1 e.1)(Dirty e.2)(Shared s.3 e.3)(Exclusive e.4) =
(Invalid e.1)(Dirty e.2)(Shared s.1 e.4 s.3 e.3)(Exclusive );
* rm_3'
C (Invalid s.1 e.1)(Dirty e.2)(Shared e.3)(Exclusive s.4 e.4) =
(Invalid e.1)(Dirty e.2)(Shared s.1 s.4 e.4 e.3)(Exclusive );
* wh_1 Trivial
* wh_2
D (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive s.4 e.4) =
(Invalid e.1)(Dirty s.4 e.2)(Shared e.3)(Exclusive e.4);
* wh_3
E (Invalid e.1)(Dirty e.2)(Shared s.3)(Exclusive e.4) =
(Invalid e.1)(Dirty e.2)(Shared )(Exclusive s.3 e.4);
* wh_4 Trivial? shared >= 2
* wm
D (Invalid s.1 e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
(Invalid e.4 e.3 e.2 e.1)(Dirty s.1)(Shared )(Exclusive );
}
Result{
(Invalid e.1)(Dirty s.2 e.2)(Shared s.3 e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty s.2 e.2)(Shared e.3)(Exclusive s.4 e.4) = False;
(Invalid e.1)(Dirty s.21 s.22 e.2)(Shared e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive s.41 s.42 e.4) = False;
(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = True;
}
Alexei Lisitsa
2005-07-14