MMgc thread safety annotations

I want to use static analysis to find race conditions in the MMGC_THREADSAFE stuff I'm working on.

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

		// ...

	}
}

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)