MMgc thread safety annotations: Difference between revisions

m
Line 129: Line 129:
A thread state expression is '''inconsistent''' if it's self-contradictory, like "(P AND NOT P)".  This means this thread state expression can never be satisfied; it's never true.  Note that "((P AND NOT P) OR Q)" is not inconsistent; it simplifies to "Q".
A thread state expression is '''inconsistent''' if it's self-contradictory, like "(P AND NOT P)".  This means this thread state expression can never be satisfied; it's never true.  Note that "((P AND NOT P) OR Q)" is not inconsistent; it simplifies to "Q".


One thread state expression may '''imply'' another, as in logic: "(P AND Q)" implies "(P OR R)".  It means any time the former is true, the latter will be true.
One thread state expression may '''imply''' another, as in logic: "(P AND Q)" implies "(P OR R)".  It means any time the former is true, the latter will be true.


=== Known thread state ===
=== Known thread state ===
638

edits