View source for MMgc thread safety annotations

This is a proposal by jorendorff to statically enforce certain aspects of thread safety in MMgc.

== Basic idea ==

I am currently adding thread safety to a complex C++ library that was not designed with thread safety in mind ([[mdc:MMgc|MMgc]]).  This involves a lot of very careful thinking about which variables are protected by which locks.

Actually it's hairier than that, because the thread safety model I'm using (the SpiderMonkey request model) has some rather ''clever'' optimizations, and the thread safety schemes that protect certain variables are often much subtler than a simple mutex.

So I've started putting annotations on each member function and each member variable of <code>class MMgc::GC</code>.  Like this:

 namespace MMgc {
 	class GC  //...
 	{
 		// ...
 
 		/** '''@access Requires(pageMapLock)''' */
 		uintptr memStart;
 		/** '''@access Requires(pageMapLock)''' */
 		uintptr memEnd;
 
 		/** '''@access Requires(m_lock)''' */
 		size_t totalGCPages;
 
 		/**
 		 * This spinlock covers memStart, memEnd, and the contents of pageMap.
 		 */
 		mutable GCSpinLock pageMapLock;
 
 		// ...
 
 		/**
 		 * Zero out the pageMap bits for the given address.
 		 *
 		 * '''@access Requires(pageMapLock)'''
 		 */
 		void ClearPageMapValue(uintptr addr);
 
 		// ...
 
 	}
 }

As it turns out, this is helpful even without static analysis.  These policies are part of the contract for every method and every variable.  They should definitely be documented, at least!

For member variables, the <code>@access</code> restriction applies to any thread trying to read or write the variable.  For member functions, it applies to the calling thread.

I also have some conditions I'd like to demand of the calling thread that aren't the names of actual lock objects.  I've been using <code>Requires(request)</code> to mean "the thread must be in a matching <code>BeginRequest</code>/<code>EndRequest</code> pair", and likewise <code>Requires(exclusiveGC)</code> means we're in "stop-the-world" mode; all application threads have stopped and the calling thread is the single thread doing GC work.

Conditions can be combined, using <code>&amp;&amp;</code> and <code>||</code>, as in:

 		/**
 		 * Points to the head of a linked list of edge callback objects.
 		 *
 		 * '''@access Requires((request && m_callbackListLock) || exclusiveGC)'''
 		 *
 		 * In an MMGC_THREADSAFE build, this linked list is protected by the
 		 * request model.  A thread must only access the list (a) from
 		 * application code that is within a request AND holds
 		 * m_callbackListLock; or (b) from MMgc code in the
 		 * m_exclusiveGCThread.
 		 *
 		 * This policy is different from the one that covers m_callbacks for
 		 * two reasons.  First, m_callbacks can fire the precollect callback
 		 * even if the calling thread is not in a request at all, so this
 		 * policy would be insufficient for m_callbacks.  Second,
 		 * m_edgeCallbacks fires very frequently during marking, so a
 		 * lock-free policy is probably much faster.
 		 */
 		GCEdgeCallback *m_edgeCallbacks;

Lastly, a <code>ReadWrite</code> access restriction indicates that one condition suffices for code that only wants to read the variable, while a different condition confers full read/write access.

 		/**
 		 * True if incremental marking is on and some objects have been marked.
 		 * This means write barriers are enabled.
 		 *
 		 * '''@access ReadWrite(request, exclusiveGC)'''
 		 *
 		 * The GC thread may read and write this flag.  Application threads in
 		 * requests have read-only access.
 		 */
 		bool marking;

—[[User:Jorend|jorendorff]] 15:12, 19 October 2007 (PDT)

Taras suggests something more like

  /**
   * True if incremental marking is on and some objects have been marked.
   * This means write barriers are enabled.
   */
  MMGC_THREADSAFE_READ_WRITE(request, exclusiveGC)
  bool marking;

—[[User:Jorend|jorendorff]] 17:21, 19 October 2007 (PDT)

'''Conjecture about <code>ReadWrite</code>.'''  If all threads actually obey the <code>ReadWrite(R, W)</code> access restriction, and the restriction itself meets the following three criteria, then I claim all accesses to the protected variable will appear to be nicely serialized.

* '''Mutual exclusion.'''  A thread being in state W implies that no other thread is in state R or state W.
* '''No deferred writes.'''  Leaving state W flushes the variable to memory.  That is, the CPU never moves a write to the protected variable past a transition out of state W.
* '''No stale reads.'''  Entering state R or state W flushes the variable from cache.  That is, the CPU never moves a transition into state R or state W past a read from the protected variable.

For the last two conditions, entering or leaving any kind of lock at those state transitions is enough.

(Elementary stuff, maybe, but I'm not used to thinking this way, so it's a big deal to me.)  (I'd like to make a stronger statement, allowing the timing of the flushes to be a little fuzzier, but can't pin it down right now.)

Note that <code>Requires(X)</code> is the same as <code>ReadWrite(X, X)</code>.  In that case, at least, the above conjecture simplifies to something obviously (heh) true.

For static analysis, the programmer could add static assertions saying things like, "<code>request</code> and <code>exclusiveGC</code> are mutually exclusive".  Given those assertions, a smart enough tool could try to prove the "mutual exclusion" condition above.  The assertions could also be checked during the abstract interpretation phase.
—[[User:Jorend|jorendorff]] 10:35, 11 April 2008 (PDT)

== Specification ==

<div class="note">This is incomplete and it has some flaws.  I'm hoping to get help from people who actually know a thing or two about using types for stuff like this.

The main flaw is that it looks pretty challenging to implement!

Another flaw is that when the static checker sees <code>REQUIRES(foo)</code>, it can't assume <code>!bar</code>.  The annotations usually mean to imply "all other state variables are false".  The semantics should change, but then users would need a way to say "<code>bar</code> may or may not be true".

Also, I recently added a thread state variable named "initializing" that seems impossible to formalize this way.  —jorendorff</div>

The goal is to prove a certain minimal consistency between what states we ''think'' a multi-threaded program can get into and what the code actually says.

We first declare a set of boolean variables that captures the status of each thread.  These are not C++ variables.  They're per-thread, not shared; and they are true-false statements about the thread, not physical memory locations.

; MMGC_TS_VAR(<var>name</var>);
: Syntactically this is a declaration, including the semicolon.  It's only legal at top-level (outside all classes, namespaces, etc.).
: Introduces a ''thread state variable'' with the given name.  Regardless of C++'s scoping rules, all thread state variables logically inhabit the same global namespace.

=== Thread state expressions ===

A '''thread state expression''' combines thread state variables with logical operators.

 tsexpr ::= ''tsvar'' | (''tsexpr'' AND ''tsexpr'') | (''tsexpr'' OR ''tsexpr'') | NOT ''tsexpr''

When a thread state expression appears in C++ code, it looks like this:

 tsexpr ::= ''tsvar''
          | MMGC_TS_OR(''tsexpr'', ''tsexpr'')
          | MMGC_TS_AND(''tsexpr'', ''tsexpr'')
          | MMGC_TS_NOT(''tsexpr'')

Same meaning, slightly different syntax.

(This is just propositional logic, which is extremely well-understood.  I'm hoping it's very 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.

:''Thread state variables should probably have optional "default values" which they assume whenever a thread state expression doesn't explicitly say either way.  For example, the variable <code>serverOnFire</code> might be false by default.  Then the expression <code>queueLock</code> could be taken as shorthand for <code>(queueLock AND NOT serverOnFire)</code>.  Of course then we'd need a way to override that default in a given expression, like <code>(inSignalHandler AND POSSIBLY serverOnFire)</code>.  The idea is, this would be a superficial feature of the annotation language.  It wouldn't affect the logic of the system.  It would just make the mapping from thread state expressions to propositional logic a bit less obvious and more intuitive. --[[User:Jorend|jorendorff]] 09:09, 19 November 2007 (PST)''

=== Known thread state ===

For a given translation unit, for each position in a function, we'll define the ''known thread state'' at that point.  The known thread state is a thread state expression.

:''The idea was to specify some kind of abstract interpretation for this, but it looks kinda hairy, and I might not be the right person to do it anyway. --[[User:Jorend|jorendorff]] 09:12, 19 November 2007 (PST)''

* At the top of a function, the known thread state is ''tsexpr'' if the function (definition or declaration) is annotated with <code>MMGC_TS_METHOD_REQUIRES(</code><var>tsexpr</var><code>)</code>, and <code>{}</code> otherwise (indicating nothing is known).

* Each arc may modify the state, as follows:

:* Stepping past an <code>MMGC_TS_TRANSITION(<var>name</var>, <var>newState</var>)</code> statement causes the variable <var>name</var> in the known state to transition from <code>!<var>newState</var></code> to <code><var>newState</var></code>.  Reaching this statement is an error if the known state (before) does not include the pair <code><var>name</var>: !<var>newState</var></code>.

:* Entering the scope of a sentry object is equivalent to stepping past an <code>MMGC_TS_TRANSITION(<var>name</var>, true)</code> statement.

:* Leaving the scope of a sentry object is equivalent to stepping past an <code>MMGC_TS_TRANSITION(<var>name</var>, false)</code> statement.

; MMGC_TS_METHOD_REQUIRES(<var>ts-expr</var>)
: .
; MMGC_TS_FIELD_REQUIRES(<var>ts-expr</var>)
: .
; MMGC_TS_FIELD_RW_REQUIRES(<var>read-ts-expr</var>, <var>write-ts-expr</var>)
: .


; MMGC_TS_LOCK(<var>name</var>)
: This is allowed before any variable declaration.
: Indicates that the variable being declared is a lock, and that the
; MMGC_TS_LOCK_SENTRY_CLASS
: This is allowed before any class declaration.
: Indicates that the class is a lock sentry class.  Objects of this class then cause state transitions to happen during flow analysis.
; MMGC_TS_TRANSITION(<var>name</var>, {true|false});
: Syntactically this is a statement, including the semicolon.
: Passing this statement causes the named thread state variable to transition to the specified value.