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

		// ...

	}
}

--jorendorff 15:12, 19 October 2007 (PDT)