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 (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 class MMgc::GC. 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 @access 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 Requires(request) to mean "the thread must be in a matching BeginRequest/EndRequest pair", and likewise Requires(exclusiveGC) 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 && and ||, 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 ReadWrite 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;

—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;

—jorendorff 17:21, 19 October 2007 (PDT)

Conjecture about ReadWrite. If all threads actually obey the ReadWrite(R, W) 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 Requires(X) is the same as ReadWrite(X, X). 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, "request and exclusiveGC 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. —jorendorff 10:35, 11 April 2008 (PDT)

Specification

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(name);

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 serverOnFire might be false by default. Then the expression queueLock could be taken as shorthand for (queueLock AND NOT serverOnFire). Of course then we'd need a way to override that default in a given expression, like (inSignalHandler AND POSSIBLY serverOnFire). 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. --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. --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 MMGC_TS_METHOD_REQUIRES(tsexpr), and {} otherwise (indicating nothing is known).

• Each arc may modify the state, as follows:

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

• Entering the scope of a sentry object is equivalent to stepping past an MMGC_TS_TRANSITION(name, true) statement.

• Leaving the scope of a sentry object is equivalent to stepping past an MMGC_TS_TRANSITION(name, false) statement.

MMGC_TS_METHOD_REQUIRES(ts-expr)

.

MMGC_TS_FIELD_REQUIRES(ts-expr)

.

MMGC_TS_FIELD_RW_REQUIRES(read-ts-expr, write-ts-expr)

.

MMGC_TS_LOCK(name)

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(name, {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.