MMgc thread safety annotations: Difference between revisions

MMgc thread safety annotations (view source)

Revision as of 14:08, 20 October 2007

1,146 bytes added , 20 October 2007

→‎Thread state expressions

Jorend

638

edits

@@ Line 103: / Line 103: @@
 === Thread state expressions ===
-A '''thread state expression''' is a logical expression that combines
+A '''thread state expression''' combines thread state variables with logical operators.
   tsexpr ::= ''tsvar'' | (''tsexpr'' AND ''tsexpr'') | (''tsexpr'' OR ''tsexpr'') | NOT ''tsexpr''
-(Note on logic:  With a few applications of the distributive law and de Morgan's laws, some double negative elimination, and a little sorting, this can be simplified to a canonical form, which is like
+When a thread state expression appears in C++ code, it looks like this:
-  tsexpr ::= sorted list of ''case''s joined by OR
+  tsexpr ::= ''tsvar''
- case  ::= sorted list of ''simple-assertion''s joined by AND
+          | MMGC_TS_OR(''tsexpr'', ''tsexpr'')
- simple-assertion ::= ''tsvar'' | NOT ''tsvar''
+          | MMGC_TS_AND(''tsexpr'', ''tsexpr'')
+          | MMGC_TS_NOT(''tsexpr'')
-Ignore the NOT symbol when you're sorting and this will put contradictions like "A AND NOT A" right next to each other like that.)
+Same meaning, slightly different syntax.
-When a thread state expression appears in C++ code, it looks like this instead:
+(Note on logic:  You can define a canonical form on thread state expressions.  Here's an algorithm that defines a particularly verbose canonical form; there are lots of ways to improve on it:
- tsexpr ::= ''tsvar'' | MMGC_TS_OR(''tsexpr'', ''tsexpr'') | MMGC_TS_AND(''tsexpr'', ''tsexpr'') | MMGC_TS_NOT(''tsexpr'')
+# Get the sorted list ''V'' of all thread state variables that appear in the expression.
+# Generate all 2<sup>|''V''|</sup> possibilities in some canonical order, e.g. if V=[A,B] then the possibilities are {A: true, B: true}, {A: true, B: false}, {A: false, B: true}, and {A: false, B: false}.
+# For each possibility, plug the values into the thread state expression and evaluate.
+# Your canonical form is a big OR-expression collecting all the possibilities for which the expression evaluates true.  For example, if the expression is true for the first three possibilities above, but not the fourth, then the canonical form is: <code>((A AND B) OR (A AND NOT B) OR (NOT A AND B))</code>.
-Same meaning, slightly different syntax.
+A smarter algorithm would make the canonical form for this expression something more like <code>(A OR B)</code>.
+A canonical form like this one that's all "multiplied out", with ORs at the top tier, any ANDs below that, and any NOTs appearing only on individual variables, is easy to work with.)
+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.
 === Known thread state ===