diff --git a/mps/code/arena.c b/mps/code/arena.c
index a3301521fae..b73e548c78d 100644
--- a/mps/code/arena.c
+++ b/mps/code/arena.c
@@ -82,6 +82,14 @@ static Res ArenaNoPagesMarkAllocated(Arena arena, Chunk chunk,
   return ResUNIMPL;
 }
 
+static Bool ArenaNoChunkPageMapped(Chunk chunk, Index index)
+{
+  UNUSED(chunk);
+  UNUSED(index);
+  NOTREACHED;
+  return FALSE;
+}
+
 static Res ArenaNoCreate(Arena *arenaReturn, ArgList args)
 {
   UNUSED(arenaReturn);
@@ -122,6 +130,7 @@ DEFINE_CLASS(Arena, AbstractArena, klass)
   klass->chunkFinish = ArenaNoChunkFinish;
   klass->compact = ArenaTrivCompact;
   klass->pagesMarkAllocated = ArenaNoPagesMarkAllocated;
+  klass->chunkPageMapped = ArenaNoChunkPageMapped;
   klass->sig = ArenaClassSig;
 }
 
@@ -144,6 +153,7 @@ Bool ArenaClassCheck(ArenaClass klass)
   CHECKL(FUNCHECK(klass->chunkFinish));
   CHECKL(FUNCHECK(klass->compact));
   CHECKL(FUNCHECK(klass->pagesMarkAllocated));
+  CHECKL(FUNCHECK(klass->chunkPageMapped));
   CHECKS(ArenaClass, klass);
   return TRUE;
 }
diff --git a/mps/code/arenacl.c b/mps/code/arenacl.c
index 72e8c4af386..757b4c7326c 100644
--- a/mps/code/arenacl.c
+++ b/mps/code/arenacl.c
@@ -383,6 +383,20 @@ static Res ClientArenaPagesMarkAllocated(Arena arena, Chunk chunk,
 }
 
 
+/* ClientChunkPageMapped -- determine if a page is mapped */
+
+static Bool ClientChunkPageMapped(Chunk chunk, Index index)
+{
+  UNUSED(chunk);
+  UNUSED(index);
+
+  AVERT(Chunk, chunk);
+  AVER(index < chunk->pages);
+
+  return TRUE;
+}
+
+
 /* ClientArenaFree - free a region in the arena */
 
 static void ClientArenaFree(Addr base, Size size, Pool pool)
@@ -443,6 +457,7 @@ DEFINE_CLASS(Arena, ClientArena, klass)
   klass->free = ClientArenaFree;
   klass->chunkInit = ClientChunkInit;
   klass->chunkFinish = ClientChunkFinish;
+  klass->chunkPageMapped = ClientChunkPageMapped;
 }
 
 
diff --git a/mps/code/arenavm.c b/mps/code/arenavm.c
index 0168b4b6ed8..78e2a67cbf4 100644
--- a/mps/code/arenavm.c
+++ b/mps/code/arenavm.c
@@ -932,6 +932,16 @@ static Res VMPagesMarkAllocated(Arena arena, Chunk chunk,
 }
 
 
+static Bool VMChunkPageMapped(Chunk chunk, Index index)
+{
+  VMChunk vmChunk;
+  AVERT(Chunk, chunk);
+  AVER(index < chunk->pages);
+  vmChunk = Chunk2VMChunk(chunk);
+  return BTGet(vmChunk->pages.mapped, index);
+}
+
+
 /* chunkUnmapAroundPage -- unmap spare pages in a chunk including this one
  *
  * Unmap the spare page passed, and possibly other pages in the chunk,
@@ -1208,6 +1218,7 @@ DEFINE_CLASS(Arena, VMArena, klass)
   klass->chunkFinish = VMChunkFinish;
   klass->compact = VMCompact;
   klass->pagesMarkAllocated = VMPagesMarkAllocated;
+  klass->chunkPageMapped = VMChunkPageMapped;
 }
 
 
diff --git a/mps/code/config.h b/mps/code/config.h
index 5b73c6d8ff3..021acf277c8 100644
--- a/mps/code/config.h
+++ b/mps/code/config.h
@@ -167,8 +167,9 @@
 /* CONFIG_THREAD_SINGLE -- support single-threaded execution only
  *
  * This symbol causes the MPS to be built for single-threaded
- * execution only, where locks are not needed and so lock operations
- * can be defined as no-ops by lock.h.
+ * execution only, where locks are not needed and so the generic
+ * ("ANSI") lock module lockan.c can be used instead of the
+ * platform-specific lock module.
  */
 
 #if !defined(CONFIG_THREAD_SINGLE)
diff --git a/mps/code/global.c b/mps/code/global.c
index 02b2f04928e..69768a6e5d5 100644
--- a/mps/code/global.c
+++ b/mps/code/global.c
@@ -409,7 +409,7 @@ void GlobalsPrepareToDestroy(Globals arenaGlobals)
   arenaGlobals->defaultChain = NULL;
   ChainDestroy(defaultChain);
 
-  LockRelease(arenaGlobals->lock);
+  ArenaLeave(arena);
   /* Theoretically, another thread could grab the lock here, but it's */
   /* not worth worrying about, since an attempt after the lock has been */
   /* destroyed would lead to a crash just the same. */
@@ -493,10 +493,9 @@ Ring GlobalsRememberedSummaryRing(Globals global)
 
 /* ArenaEnter -- enter the state where you can look at the arena */
 
-void (ArenaEnter)(Arena arena)
+void ArenaEnter(Arena arena)
 {
-  AVERT(Arena, arena);
-  ArenaEnter(arena);
+  ArenaEnterLock(arena, FALSE);
 }
 
 /*  The recursive argument specifies whether to claim the lock
@@ -541,10 +540,10 @@ void ArenaEnterRecursive(Arena arena)
 
 /* ArenaLeave -- leave the state where you can look at MPM data structures */
 
-void (ArenaLeave)(Arena arena)
+void ArenaLeave(Arena arena)
 {
   AVERT(Arena, arena);
-  ArenaLeave(arena);
+  ArenaLeaveLock(arena, FALSE);
 }
 
 void ArenaLeaveLock(Arena arena, Bool recursive)
@@ -574,6 +573,12 @@ void ArenaLeaveRecursive(Arena arena)
   ArenaLeaveLock(arena, TRUE);
 }
 
+Bool ArenaBusy(Arena arena)
+{
+  return LockIsHeld(ArenaGlobals(arena)->lock);
+}
+
+
 /* mps_exception_info -- pointer to exception info
  *
  * This is a hack to make exception info easier to find in a release
diff --git a/mps/code/lock.h b/mps/code/lock.h
index 35d0ed6db41..1a02d7997ed 100644
--- a/mps/code/lock.h
+++ b/mps/code/lock.h
@@ -78,6 +78,11 @@ extern void LockRelease(Lock lock);
 extern Bool LockCheck(Lock lock);
 
 
+/* LockIsHeld -- test whether lock is held by any thread */
+
+extern Bool LockIsHeld(Lock lock);
+
+
 /*  == Global locks == */
 
 
@@ -123,26 +128,6 @@ extern void LockClaimGlobal(void);
 extern void LockReleaseGlobal(void);
 
 
-#if defined(LOCK)
-/* Nothing to do: functions declared in all lock configurations. */
-#elif defined(LOCK_NONE)
-#define LockSize() MPS_PF_ALIGN
-#define LockInit(lock) UNUSED(lock)
-#define LockFinish(lock) UNUSED(lock)
-#define LockClaimRecursive(lock) UNUSED(lock)
-#define LockReleaseRecursive(lock) UNUSED(lock)
-#define LockClaim(lock) UNUSED(lock)
-#define LockRelease(lock) UNUSED(lock)
-#define LockCheck(lock) ((void)lock, TRUE)
-#define LockClaimGlobalRecursive()
-#define LockReleaseGlobalRecursive()
-#define LockClaimGlobal()
-#define LockReleaseGlobal()
-#else
-#error "No lock configuration."
-#endif  /* LOCK */
-
-
 #endif /* lock_h */
 
 
diff --git a/mps/code/lockan.c b/mps/code/lockan.c
index fe5082a6ebf..8b1b61a5243 100644
--- a/mps/code/lockan.c
+++ b/mps/code/lockan.c
@@ -79,6 +79,12 @@ void (LockReleaseRecursive)(Lock lock)
   --lock->claims;
 }
 
+Bool (LockIsHeld)(Lock lock)
+{
+  AVERT(Lock, lock);
+  return lock->claims > 0;
+}
+
 
 /* Global locking is performed by normal locks.
  * A separate lock structure is used for recursive and
diff --git a/mps/code/lockcov.c b/mps/code/lockcov.c
index 84866046d82..af225d07c40 100644
--- a/mps/code/lockcov.c
+++ b/mps/code/lockcov.c
@@ -39,20 +39,28 @@ int main(int argc, char *argv[])
   Insist(b != NULL);
 
   LockInit(a);
+  Insist(!LockIsHeld(a));
   LockInit(b);
+  Insist(!LockIsHeld(b));
   LockClaimGlobal();
   LockClaim(a);
+  Insist(LockIsHeld(a));
   LockClaimRecursive(b);
+  Insist(LockIsHeld(b));
   LockClaimGlobalRecursive();
   LockReleaseGlobal();
   LockClaimGlobal();
   LockRelease(a);
+  Insist(!LockIsHeld(a));
   LockClaimGlobalRecursive();
   LockReleaseGlobal();
   LockClaimRecursive(b);
+  Insist(LockIsHeld(b));
   LockFinish(a);
   LockReleaseRecursive(b);
+  Insist(LockIsHeld(b));
   LockReleaseRecursive(b);
+  Insist(!LockIsHeld(b));
   LockFinish(b);
   LockInit(a);
   LockClaim(a);
diff --git a/mps/code/lockix.c b/mps/code/lockix.c
index 5b166fdc625..4c42d754ba2 100644
--- a/mps/code/lockix.c
+++ b/mps/code/lockix.c
@@ -45,6 +45,7 @@
 
 SRCID(lockix, "$Id$");
 
+#if defined(LOCK)
 
 /* LockStruct -- the MPS lock structure
  *
@@ -185,6 +186,21 @@ void (LockReleaseRecursive)(Lock lock)
 }
 
 
+/* LockIsHeld -- test whether lock is held */
+
+Bool (LockIsHeld)(Lock lock)
+{
+  AVERT(Lock, lock);
+  if (pthread_mutex_trylock(&lock->mut) == 0) {
+    Bool claimed = lock->claims > 0;
+    int res = pthread_mutex_unlock(&lock->mut);
+    AVER(res == 0);
+    return claimed;
+  }
+  return TRUE;
+}
+
+
 /* Global locks
  *
  * .global: The two "global" locks are statically allocated normal locks.
@@ -245,6 +261,13 @@ void (LockReleaseGlobal)(void)
 }
 
 
+#elif defined(LOCK_NONE)
+#include "lockan.c"
+#else
+#error "No lock configuration."
+#endif
+
+
 /* C. COPYRIGHT AND LICENSE
  *
  * Copyright (C) 2001-2016 Ravenbrook Limited <http://www.ravenbrook.com/>.
diff --git a/mps/code/lockw3.c b/mps/code/lockw3.c
index daf2473d4e3..a471687514e 100644
--- a/mps/code/lockw3.c
+++ b/mps/code/lockw3.c
@@ -31,6 +31,7 @@
 
 SRCID(lockw3, "$Id$");
 
+#if defined(LOCK)
 
 /* .lock.win32: Win32 lock structure; uses CRITICAL_SECTION */
 typedef struct LockStruct {
@@ -103,6 +104,15 @@ void (LockReleaseRecursive)(Lock lock)
   LeaveCriticalSection(&lock->cs);
 }
 
+Bool (LockIsHeld)(Lock lock)
+{
+  if (TryEnterCriticalSection(&lock->cs)) {
+    Bool claimed = lock->claims > 0;
+    LeaveCriticalSection(&lock->cs);
+    return claimed;
+  }
+  return TRUE;
+}
 
 
 /* Global locking is performed by normal locks.
@@ -156,6 +166,13 @@ void (LockReleaseGlobal)(void)
 }
 
 
+#elif defined(LOCK_NONE)
+#include "lockan.c"
+#else
+#error "No lock configuration."
+#endif
+
+
 /* C. COPYRIGHT AND LICENSE
  *
  * Copyright (C) 2001-2016 Ravenbrook Limited <http://www.ravenbrook.com/>.
diff --git a/mps/code/mpm.h b/mps/code/mpm.h
index 9f5f3365fa4..e2b99e1fead 100644
--- a/mps/code/mpm.h
+++ b/mps/code/mpm.h
@@ -488,7 +488,6 @@ extern Bool ArenaAccess(Addr addr, AccessSet mode, MutatorFaultContext context);
 extern Res ArenaFreeLandInsert(Arena arena, Addr base, Addr limit);
 extern void ArenaFreeLandDelete(Arena arena, Addr base, Addr limit);
 
-
 extern Bool GlobalsCheck(Globals arena);
 extern Res GlobalsInit(Globals arena);
 extern void GlobalsFinish(Globals arena);
@@ -524,16 +523,12 @@ extern Bool ArenaGrainSizeCheck(Size size);
 extern void ArenaEnterLock(Arena arena, Bool recursive);
 extern void ArenaLeaveLock(Arena arena, Bool recursive);
 
-extern void (ArenaEnter)(Arena arena);
-extern void (ArenaLeave)(Arena arena);
+extern void ArenaEnter(Arena arena);
+extern void ArenaLeave(Arena arena);
 extern void (ArenaPoll)(Globals globals);
 
 #if defined(SHIELD)
-#define ArenaEnter(arena)  ArenaEnterLock(arena, FALSE)
-#define ArenaLeave(arena)  ArenaLeaveLock(arena, FALSE)
 #elif defined(SHIELD_NONE)
-#define ArenaEnter(arena)  UNUSED(arena)
-#define ArenaLeave(arena)  AVER(arena->busyTraces == TraceSetEMPTY)
 #define ArenaPoll(globals)  UNUSED(globals)
 #else
 #error "No shield configuration."
@@ -546,10 +541,12 @@ extern Bool (ArenaStep)(Globals globals, double interval, double multiplier);
 extern void ArenaClamp(Globals globals);
 extern void ArenaRelease(Globals globals);
 extern void ArenaPark(Globals globals);
+extern void ArenaPostmortem(Globals globals);
 extern void ArenaExposeRemember(Globals globals, Bool remember);
 extern void ArenaRestoreProtection(Globals globals);
 extern Res ArenaStartCollect(Globals globals, int why);
 extern Res ArenaCollect(Globals globals, int why);
+extern Bool ArenaBusy(Arena arena);
 extern Bool ArenaHasAddr(Arena arena, Addr addr);
 extern Res ArenaAddrObject(Addr *pReturn, Arena arena, Addr addr);
 extern void ArenaChunkInsert(Arena arena, Chunk chunk);
@@ -895,7 +892,7 @@ extern void (ShieldFlush)(Arena arena);
 #define ShieldLower(arena, seg, mode) \
   BEGIN UNUSED(arena); UNUSED(seg); UNUSED(mode); END
 #define ShieldEnter(arena) BEGIN UNUSED(arena); END
-#define ShieldLeave(arena) BEGIN UNUSED(arena); END
+#define ShieldLeave(arena) AVER(arena->busyTraces == TraceSetEMPTY)
 #define ShieldExpose(arena, seg)  \
   BEGIN UNUSED(arena); UNUSED(seg); END
 #define ShieldCover(arena, seg) \
diff --git a/mps/code/mpmst.h b/mps/code/mpmst.h
index 04c19f63e92..dd0ecd077fc 100644
--- a/mps/code/mpmst.h
+++ b/mps/code/mpmst.h
@@ -504,6 +504,7 @@ typedef struct mps_arena_class_s {
   ArenaChunkFinishMethod chunkFinish;
   ArenaCompactMethod compact;
   ArenaPagesMarkAllocatedMethod pagesMarkAllocated;
+  ArenaChunkPageMappedMethod chunkPageMapped;
   Sig sig;
 } ArenaClassStruct;
 
diff --git a/mps/code/mpmtypes.h b/mps/code/mpmtypes.h
index d1180ea9a8d..5d6ce41ff08 100644
--- a/mps/code/mpmtypes.h
+++ b/mps/code/mpmtypes.h
@@ -124,6 +124,7 @@ typedef void (*ArenaCompactMethod)(Arena arena, Trace trace);
 typedef Res (*ArenaPagesMarkAllocatedMethod)(Arena arena, Chunk chunk,
                                              Index baseIndex, Count pages,
                                              Pool pool);
+typedef Bool (*ArenaChunkPageMappedMethod)(Chunk chunk, Index index);
 
 
 /* These are not generally exposed and public, but are part of a commercial
diff --git a/mps/code/mps.h b/mps/code/mps.h
index 6aeffd2962d..c9ecab4cfae 100644
--- a/mps/code/mps.h
+++ b/mps/code/mps.h
@@ -435,6 +435,7 @@ typedef struct mps_fmt_fixed_s {
 extern void mps_arena_clamp(mps_arena_t);
 extern void mps_arena_release(mps_arena_t);
 extern void mps_arena_park(mps_arena_t);
+extern void mps_arena_postmortem(mps_arena_t);
 extern void mps_arena_expose(mps_arena_t);
 extern void mps_arena_unsafe_expose_remember_protection(mps_arena_t);
 extern void mps_arena_unsafe_restore_protection(mps_arena_t);
@@ -460,6 +461,7 @@ extern size_t mps_arena_spare_commit_limit(mps_arena_t);
 extern double mps_arena_pause_time(mps_arena_t);
 extern void mps_arena_pause_time_set(mps_arena_t, double);
 
+extern mps_bool_t mps_arena_busy(mps_arena_t);
 extern mps_bool_t mps_arena_has_addr(mps_arena_t, mps_addr_t);
 extern mps_bool_t mps_addr_pool(mps_pool_t *, mps_arena_t, mps_addr_t);
 extern mps_bool_t mps_addr_fmt(mps_fmt_t *, mps_arena_t, mps_addr_t);
diff --git a/mps/code/mpsi.c b/mps/code/mpsi.c
index 9ae6fcbfa97..3449c1aaed6 100644
--- a/mps/code/mpsi.c
+++ b/mps/code/mpsi.c
@@ -260,6 +260,15 @@ void mps_arena_park(mps_arena_t arena)
 }
 
 
+void mps_arena_postmortem(mps_arena_t arena)
+{
+  /* Don't call ArenaEnter -- one of the purposes of this function is
+   * to release the arena lock if it's held */
+  AVER(TESTT(Arena, arena));
+  ArenaPostmortem(ArenaGlobals(arena));
+}
+
+
 void mps_arena_expose(mps_arena_t arena)
 {
   ArenaEnter(arena);
@@ -374,6 +383,17 @@ void mps_arena_destroy(mps_arena_t arena)
 }
 
 
+/* mps_arena_busy -- is the arena part way through an operation? */
+
+mps_bool_t mps_arena_busy(mps_arena_t arena)
+{
+  /* Don't call ArenaEnter -- the purpose of this function is to
+   * determine if the arena lock is held */
+  AVER(TESTT(Arena, arena));
+  return ArenaBusy(arena);
+}
+
+
 /* mps_arena_has_addr -- is this address managed by this arena? */
 
 mps_bool_t mps_arena_has_addr(mps_arena_t arena, mps_addr_t p)
diff --git a/mps/code/mpsicv.c b/mps/code/mpsicv.c
index d1a9759a3b8..0df2c4bc0c7 100644
--- a/mps/code/mpsicv.c
+++ b/mps/code/mpsicv.c
@@ -450,11 +450,13 @@ static void *test(void *arg, size_t s)
     mps_word_t c;
     size_t r;
 
+    Insist(!mps_arena_busy(arena));
+
     c = mps_collections(arena);
 
     if(collections != c) {
       collections = c;
-      printf("\nCollection %"PRIuLONGEST", %lu objects.\n", (ulongest_t)c, i);
+      printf("Collection %"PRIuLONGEST", %lu objects.\n", (ulongest_t)c, i);
       for(r = 0; r < exactRootsCOUNT; ++r) {
         cdie(exactRoots[r] == objNULL || dylan_check(exactRoots[r]),
              "all roots check");
@@ -565,7 +567,7 @@ int main(int argc, char *argv[])
     MPS_ARGS_ADD(args, MPS_KEY_PAUSE_TIME, rnd_pause_time());
     MPS_ARGS_ADD(args, MPS_KEY_ARENA_SIZE, TEST_ARENA_SIZE);
     die(mps_arena_create_k(&arena, mps_arena_class_vm(), args),
-        "arena_create\n");
+        "arena_create");
   } MPS_ARGS_END(args);
   die(mps_thread_reg(&thread, arena), "thread_reg");
 
@@ -591,9 +593,17 @@ int main(int argc, char *argv[])
   }
 
   mps_tramp(&r, test, arena, 0);
-  mps_root_destroy(reg_root);
-  mps_thread_dereg(thread);
-  mps_arena_destroy(arena);
+  switch (rnd() % 2) {
+  default:
+  case 0:
+    mps_root_destroy(reg_root);
+    mps_thread_dereg(thread);
+    mps_arena_destroy(arena);
+    break;
+  case 1:
+    mps_arena_postmortem(arena);
+    break;
+  }
 
   printf("%s: Conclusion: Failed to find any defects.\n", argv[0]);
   return 0;
diff --git a/mps/code/qs.c b/mps/code/qs.c
index 2a62a5ef71a..9e3089b3a89 100644
--- a/mps/code/qs.c
+++ b/mps/code/qs.c
@@ -457,6 +457,7 @@ static mps_res_t scan1(mps_ss_t ss, mps_addr_t *objectIO)
 
 static mps_res_t scan(mps_ss_t ss, mps_addr_t base, mps_addr_t limit)
 {
+  Insist(mps_arena_busy(arena));
   while(base < limit) {
     mps_res_t res;
 
diff --git a/mps/code/tagtest.c b/mps/code/tagtest.c
index 62df8ee2b1d..9b3dea53c60 100644
--- a/mps/code/tagtest.c
+++ b/mps/code/tagtest.c
@@ -77,9 +77,12 @@ static void pad(mps_addr_t addr, size_t size)
   }
 }
 
+static mps_arena_t arena;
+
 static mps_res_t scan(mps_ss_t ss, mps_addr_t base,
                       mps_addr_t limit)
 {
+  Insist(mps_arena_busy(arena));
   MPS_SCAN_BEGIN(ss) {
     mps_word_t *p = base;
     while (p < (mps_word_t *)limit) {
@@ -106,7 +109,7 @@ static mps_addr_t skip(mps_addr_t addr)
 }
 
 
-static void collect(mps_arena_t arena, size_t expected)
+static void collect(size_t expected)
 {
   size_t finalized = 0;
   mps_arena_collect(arena);
@@ -148,7 +151,6 @@ static const char *mode_name[] = {
 
 static void test(int mode)
 {
-  mps_arena_t arena;
   mps_thr_t thread;
   mps_root_t root;
   mps_fmt_t fmt;
@@ -214,7 +216,7 @@ static void test(int mode)
     die(mps_finalize(arena, &addr), "finalize");
   }
 
-  collect(arena, expected);
+  collect(expected);
 
   mps_arena_park(arena);
   mps_ap_destroy(ap);
diff --git a/mps/code/traceanc.c b/mps/code/traceanc.c
index 52761e02092..5326c5f2e21 100644
--- a/mps/code/traceanc.c
+++ b/mps/code/traceanc.c
@@ -530,12 +530,11 @@ void TraceIdMessagesDestroy(Arena arena, TraceId ti)
 
 
 
-/* --------  ArenaRelease, ArenaClamp, ArenaPark  -------- */
+/* -----  ArenaRelease, ArenaClamp, ArenaPark, ArenaPostmortem  ----- */
 
 
-/* ArenaRelease, ArenaClamp, ArenaPark -- allow/prevent collection work.
- *
- * These functions allow or prevent collection work.
+/* ArenaRelease, ArenaClamp, ArenaPark, ArenaPostmortem --
+ * allow/prevent collection work.
  */
 
 
@@ -596,6 +595,62 @@ void ArenaPark(Globals globals)
   AVER(!ArenaEmergency(arena));
 }
 
+
+/* arenaExpose -- discard all protection from MPS-managed memory
+ * 
+ * This is called by ArenaPostmortem, which we expect only to be used
+ * after a fatal error. So we use the lowest-level description of the
+ * MPS-managed memory (the chunk ring page tables) to avoid the risk
+ * of higher-level structures (like the segments) having been
+ * corrupted.
+ *
+ * After calling this function memory may not be in a consistent
+ * state, so it is not safe to continue running the MPS. If you need
+ * to expose memory but continue running the MPS, use
+ * ArenaExposeRemember instead.
+ */
+
+static void arenaExpose(Arena arena)
+{
+  Ring node, next;
+  RING_FOR(node, &arena->chunkRing, next) {
+    Chunk chunk = RING_ELT(Chunk, arenaRing, node);
+    Index i;
+    for (i = 0; i < chunk->pages; ++i) {
+      if (Method(Arena, arena, chunkPageMapped)(chunk, i)) {
+        ProtSet(PageIndexBase(chunk, i), PageIndexBase(chunk, i + 1),
+                AccessSetEMPTY);
+      }
+    }
+  }
+}
+
+
+/* ArenaPostmortem -- enter the postmortem state */
+
+void ArenaPostmortem(Globals globals)
+{
+  Arena arena = GlobalsArena(globals);
+
+  /* Ensure lock is released. */
+  while (LockIsHeld(globals->lock)) {
+    LockReleaseRecursive(globals->lock);
+  }
+
+  /* Remove the arena from the global arena ring so that it no longer
+   * handles protection faults. (Don't call arenaDenounce because that
+   * needs to claim the global ring lock, but that might already be
+   * held, for example if we are inside ArenaAccess.) */
+  RingRemove(&globals->globalRing);
+
+  /* Clamp the arena so that ArenaPoll does nothing. */
+  ArenaClamp(globals);
+
+  /* Remove all protection from mapped pages. */
+  arenaExpose(arena);
+}
+
+
 /* ArenaStartCollect -- start a collection of everything in the
  * arena; leave unclamped. */
 
diff --git a/mps/design/config.txt b/mps/design/config.txt
index 458ccdfe890..3bf1d96e29c 100644
--- a/mps/design/config.txt
+++ b/mps/design/config.txt
@@ -542,7 +542,8 @@ platform instead.
 
 _`.opt.thread`: ``CONFIG_THREAD_SINGLE`` causes the MPS to be built
 for single-threaded execution only, where locks are not needed and so
-lock operations can be defined as no-ops by ``lock.h``.
+the generic ("ANSI") lock module ``lockan.c`` can be used instead of
+the platform-specific lock module.
 
 _`.opt.poll`: ``CONFIG_POLL_NONE`` causes the MPS to be built without
 support for polling. This means that garbage collections will only
diff --git a/mps/design/lock.txt b/mps/design/lock.txt
index 6dc4e55de15..45737737bb4 100644
--- a/mps/design/lock.txt
+++ b/mps/design/lock.txt
@@ -59,6 +59,13 @@ be claimed again by the thread currently holding them, without
 blocking or deadlocking. (This is needed to implement the global
 recursive lock.)
 
+_`.req.held`: Provide a means to test if a lock is held. (This is
+needed for debugging a dynamic function table callback on Windows on
+x86-64. See ``mps_arena_busy()`` for a detailed description of this
+use case. Note that in this use case the program is running
+single-threaded and so there is no need for this feature to be
+thread-safe.)
+
 _`.req.global`: Provide *global* locks: that is locks that need not be
 allocated or initialized by the user.
 
@@ -124,6 +131,11 @@ thread and claims the lock (if not already held).
 Restores the previous state of the lock remembered by the
 corresponding ``LockClaimRecursive()`` call.
 
+``Bool LockIsHeld(Lock lock)``
+
+Return true if the lock is held by any thread, false otherwise. Note
+that this function need not be thread-safe (see `.req.held`_).
+
 ``void LockClaimGlobal(void)``
 
 Claims ownership of the binary global lock which was previously not
diff --git a/mps/manual/source/glossary/c.rst b/mps/manual/source/glossary/c.rst
index 2165bac2394..478276e619b 100644
--- a/mps/manual/source/glossary/c.rst
+++ b/mps/manual/source/glossary/c.rst
@@ -193,14 +193,14 @@ Memory Management Glossary: C
 
         .. mps:specific::
 
-            One of the three states an :term:`arena` can be in (the
-            others being the :term:`unclamped state` and the
-            :term:`parked state`). In the clamped state, no object
-            motion occurs and the staleness of :term:`location
-            dependencies` does not change. However, a :term:`garbage
-            collection` may be in progress. Call
-            :c:func:`mps_arena_clamp` to put an arena into the clamped
-            state.
+            One of the four states an :term:`arena` can be in (the
+            others being the :term:`unclamped state`, the
+            :term:`parked state`, and the :term:`postmortem state`).
+            In the clamped state, no object motion occurs and the
+            staleness of :term:`location dependencies` does not
+            change. However, a :term:`garbage collection` may be in
+            progress. Call :c:func:`mps_arena_clamp` to put an arena
+            into the clamped state.
 
     client arena
 
diff --git a/mps/manual/source/glossary/index.rst b/mps/manual/source/glossary/index.rst
index ab67f3077ec..10b76d801a7 100644
--- a/mps/manual/source/glossary/index.rst
+++ b/mps/manual/source/glossary/index.rst
@@ -410,6 +410,7 @@ All
 :term:`pointer`
 :term:`pool`
 :term:`pool class`
+:term:`postmortem state`
 :term:`precise garbage collection <exact garbage collection>`
 :term:`precise reference <exact reference>`
 :term:`precise root <exact root>`
diff --git a/mps/manual/source/glossary/p.rst b/mps/manual/source/glossary/p.rst
index 4ca1dbcd275..f968a6471d0 100644
--- a/mps/manual/source/glossary/p.rst
+++ b/mps/manual/source/glossary/p.rst
@@ -179,14 +179,15 @@ Memory Management Glossary: P
 
         .. mps:specific::
 
-            One of the three states an :term:`arena` can be in (the
-            others being the :term:`clamped state` and the
-            :term:`unclamped state`). In the parked state, no
-            :term:`garbage collection` is in progress, no object
-            motion occurs and the staleness of :term:`location
-            dependencies` does not change. Call
-            :c:func:`mps_arena_park` or :c:func:`mps_arena_collect` to
-            put an arena into the parked state.
+            One of the four states an :term:`arena` can be in (the
+            others being the :term:`clamped state`, the
+            :term:`postmortem state`, and the :term:`unclamped
+            state`). In the parked state, no :term:`garbage
+            collection` is in progress, no object motion occurs and
+            the staleness of :term:`location dependencies` does not
+            change. Call :c:func:`mps_arena_park` or
+            :c:func:`mps_arena_collect` to put an arena into the
+            parked state.
 
     perfect fit
 
@@ -402,6 +403,21 @@ Memory Management Glossary: P
             class of :term:`pools` that manage memory according to
             particular policy. See :ref:`pool`.
 
+    postmortem state
+
+        .. mps:specific::
+
+            One of the four states an :term:`arena` can be in (the
+            others being the :term:`unclamped state`, the
+            :term:`clamped state`, and the :term:`parked state`). In
+            the postmortem state, objects do not move in memory, the
+            staleness of :term:`location dependencies` does not
+            change, memory occupied by :term:`unreachable` objects is
+            not recycled, all memory protection is removed, and memory
+            may be in an inconsistent state. Call
+            :c:func:`mps_arena_postmortem` to put an arena into the
+            postmortem state.
+
     precise garbage collection
 
         .. see:: :term:`exact garbage collection`.
diff --git a/mps/manual/source/glossary/u.rst b/mps/manual/source/glossary/u.rst
index 71f8fe78ac3..756ed88bc33 100644
--- a/mps/manual/source/glossary/u.rst
+++ b/mps/manual/source/glossary/u.rst
@@ -49,12 +49,12 @@ Memory Management Glossary: U
 
         .. mps:specific::
 
-            One of the three states an :term:`arena` can be in (the
-            others being the :term:`clamped state` and the
-            :term:`parked state`). In the unclamped state, object
-            motion and other background activity may occur. Call
-            :c:func:`mps_arena_release` to put an arena into the
-            unclamped state.
+            One of the four states an :term:`arena` can be in (the
+            others being the :term:`clamped state`, the :term:`parked
+            state` and the :term:`postmortem state`). In the unclamped
+            state, object motion and other background activity may
+            occur. Call :c:func:`mps_arena_release` to put an arena
+            into the unclamped state.
 
     undead
 
diff --git a/mps/manual/source/guide/debug.rst b/mps/manual/source/guide/debug.rst
index 3c1678e660b..a922ad35af7 100644
--- a/mps/manual/source/guide/debug.rst
+++ b/mps/manual/source/guide/debug.rst
@@ -94,6 +94,31 @@ General debugging advice
    On OS X, barrier hits do not use signals and so do not enter the
    debugger.
 
+#. .. index::
+       single: postmortem debugging
+       single: postmortem state
+
+   If the :term:`client program` is stopped in the debugger with the
+   MPS part of the way through execution of an operation in an
+   :term:`arena` (for example, a crash inside a :term:`scan method`),
+   it will not be possible to call introspection functions, such as
+   :c:func:`mps_arena_has_addr` or :c:func:`mps_addr_pool` (because
+   the MPS is not re-entrant), and it may not be possible to examine
+   some regions of memory (because they are :term:`protected` by the
+   MPS).
+
+   If you are in this situation and would like to be able to call MPS
+   functions or examine regions of memory from the debugger, then you
+   can put the arena into the :term:`postmortem state` by calling
+   :c:func:`mps_arena_postmortem` from the debugger. This unlocks the
+   arena and turns off protection.
+
+   .. warning:: 
+
+       After calling :c:func:`mps_arena_postmortem`, MPS-managed
+       memory is not in a consistent state, and so it is not safe to
+       continue running the client program.
+
 
 .. index::
       single: ASLR
diff --git a/mps/manual/source/release.rst b/mps/manual/source/release.rst
index 5f73f0ad5b7..831f123cc36 100644
--- a/mps/manual/source/release.rst
+++ b/mps/manual/source/release.rst
@@ -25,6 +25,12 @@ New features
 
    .. _LinuxThreads: http://pauillac.inria.fr/~xleroy/linuxthreads/
 
+#. New function :c:func:`mps_arena_postmortem` assists with postmortem
+   debugging.
+
+#. New function :c:func:`mps_arena_busy` assists debugging of re-entry
+   errors in dynamic function table callbacks on Windows on x86-64.
+
 
 Interface changes
 .................
diff --git a/mps/manual/source/topic/arena.rst b/mps/manual/source/topic/arena.rst
index f1386781572..a64c468325a 100644
--- a/mps/manual/source/topic/arena.rst
+++ b/mps/manual/source/topic/arena.rst
@@ -430,12 +430,10 @@ Arena properties
     operating system.
 
     The function :c:func:`mps_arena_committed` may be called whatever
-    state the the arena is in (:term:`unclamped <unclamped state>`,
-    :term:`clamped <clamped state>`, or :term:`parked <parked
-    state>`). If it is called when the arena is in the unclamped state
-    then the value may change after this function returns. A possible
-    use might be to call it just after :c:func:`mps_arena_collect` to
-    estimate the size of the heap.
+    state the the arena is in. If it is called when the arena is in
+    the :term:`unclamped state` then the value may change after this
+    function returns. A possible use might be to call it just after
+    :c:func:`mps_arena_collect` to estimate the size of the heap.
 
     If you want to know how much memory the MPS is using then you're
     probably interested in the value :c:func:`mps_arena_committed` −
@@ -649,21 +647,41 @@ An arena is always in one of three states.
    The *parked state* is the same as the clamped state, with the
    additional constraint that no garbage collections are in progress.
 
+#. .. index::
+      single: arena; postmortem state
+      single: postmortem state
+
+   In the *postmortem state*, incremental collection does not take
+   place, objects do not move in memory, references do not change, the
+   staleness of :term:`location dependencies` does not change, and
+   memory occupied by :term:`unreachable` objects is not recycled.
+   Additionally, all memory protection is removed, and memory may be
+   in an inconsistent state.
+
+   .. warning::
+
+       In this state, memory managed by the arena is not in a
+       consistent state, and so it is not safe to continue running the
+       client program. This state is intended for postmortem debugging
+       only.
+
+
 Here's a summary:
 
-============================================ ================================== ============================= ===========================
-State                                        unclamped                          clamped                       parked
-============================================ ================================== ============================= ===========================
-Collections may be running?                  yes                                yes                           no
-New collections may start?                   yes                                no                            no
-Objects may move?                            yes                                no                            no
-Location dependencies may become stale?      yes                                no                            no
-Memory may be returned to the OS?            yes                                no                            no
-Functions that leave the arena in this state :c:func:`mps_arena_create_k`,      :c:func:`mps_arena_clamp`,    :c:func:`mps_arena_park`,
+============================================ ================================== ============================= =========================== ==============================
+State                                        unclamped                          clamped                       parked                      postmortem
+============================================ ================================== ============================= =========================== ==============================
+Collections may be running?                  yes                                yes                           no                          yes
+New collections may start?                   yes                                no                            no                          no
+Objects may move?                            yes                                no                            no                          no
+Location dependencies may become stale?      yes                                no                            no                          no
+Memory may be returned to the OS?            yes                                no                            no                          no
+Safe to continue running?                    yes                                yes                           yes                         no
+Functions that leave the arena in this state :c:func:`mps_arena_create_k`,      :c:func:`mps_arena_clamp`,    :c:func:`mps_arena_park`,   :c:func:`mps_arena_postmortem`
                                              :c:func:`mps_arena_release`,       :c:func:`mps_arena_step`      :c:func:`mps_arena_collect`
-                                             :c:func:`mps_arena_start_collect`, 
-                                             :c:func:`mps_arena_step`           
-============================================ ================================== ============================= ===========================
+                                             :c:func:`mps_arena_start_collect`,
+                                             :c:func:`mps_arena_step`
+============================================ ================================== ============================= =========================== ==============================
 
 The clamped and parked states are important when introspecting and
 debugging. If you are examining the contents of the heap, you don't
@@ -688,7 +706,7 @@ can only be called in this state.
 
     Put an :term:`arena` into the :term:`clamped state`.
 
-    ``arena`` is the arena to clamp.
+    ``arena`` is the arena.
 
     In the clamped state, no object motion will occur and the
     staleness of :term:`location dependencies` will not change. All
@@ -706,7 +724,7 @@ can only be called in this state.
 
     Put an :term:`arena` into the :term:`parked state`.
 
-    ``arena`` is the arena to park.
+    ``arena`` is the arena.
 
     While an arena is parked, no object motion will occur and the
     staleness of :term:`location dependencies` will not change. All
@@ -720,14 +738,42 @@ can only be called in this state.
 
 .. c:function:: void mps_arena_release(mps_arena_t arena)
 
-    Puts an arena into the :term:`unclamped state`.
+    Put an arena into the :term:`unclamped state`.
 
-    ``arena`` is the arena to unclamp.
+    ``arena`` is the arena.
 
     While an arena is unclamped, :term:`garbage collection`, object
     motion, and other background activity can take place.
 
 
+.. c:function:: void mps_arena_postmortem(mps_arena_t arena)
+
+    Put an arena into the :term:`postmortem state`.
+
+    ``arena`` is the arena.
+
+    In the postmortem state, incremental collection does not take
+    place, objects do not move in memory, references do not change,
+    the staleness of :term:`location dependencies` does not change,
+    and memory occupied by :term:`unreachable` objects is not
+    recycled. Additionally, all memory protection is removed, and
+    memory may be in an inconsistent state.
+
+    .. warning::
+
+       1. After calling this function, memory managed by the arena is
+          not in a consistent state, and so it is no longer safe to
+          continue running the client program. This functions is
+          intended for postmortem debugging only.
+
+       2. This function must be called from the thread that holds the
+          arena lock (if any thread holds it). This is the case if the
+          program is single-threaded, or if it is called from an MPS
+          assertion handler. When calling this function from the
+          debugger, check the stack to see which thread has the MPS
+          arena lock.
+
+
 .. index::
    single: garbage collection; running
    single: collection; running
@@ -885,9 +931,10 @@ application.
 
 .. index::
    pair: arena; introspection
+   pair: arena; debugging
 
-Arena introspection
--------------------
+Arena introspection and debugging
+---------------------------------
 
 .. note::
 
@@ -903,6 +950,51 @@ Arena introspection
       address belongs.
 
 
+.. c:function:: mps_bool_t mps_arena_busy(mps_arena_t arena)
+
+    Return true if an :term:`arena` is part of the way through
+    execution of an operation, false otherwise.
+
+    ``arena`` is the arena.
+
+    .. note::
+
+        This function is intended to assist with debugging fatal
+        errors in the :term:`client program`. It is not expected to be
+        needed in normal use. If you find yourself wanting to use this
+        function other than in the use case described below, there may
+        be a better way to meet your requirements: please
+        :ref:`contact us <contact>`.
+
+        A debugger running on Windows on x86-64 needs to decode the
+        call stack, which it does by calling a callback that was
+        previously installed in the dynamic function table using
+        |RtlInstallFunctionTableCallback|_. If the debugger is entered
+        while the arena is busy, and if the callback needs to read
+        from MPS-managed memory, then it may attempt to re-enter the
+        MPS, which will fail as the MPS is not re-entrant.
+
+        .. |RtlInstallFunctionTableCallback| replace:: ``RtlInstallFunctionTableCallback()``
+        .. _RtlInstallFunctionTableCallback: https://msdn.microsoft.com/en-us/library/windows/desktop/ms680595(v=vs.85).aspx
+
+        If this happens, in order to allow the debugger to finish
+        decoding the call stack, the only remedy is to put the arena
+        into the :term:`postmortem state`, so that memory is
+        :term:`unprotected` and objects do not move. So in your
+        dynamic function table callback, you might write::
+
+            if (mps_arena_busy(arena)) {
+                mps_arena_postmortem(arena);
+            }
+
+    .. warning::
+
+        This function only gives a reliable result in single-threaded
+        programs, and in multi-threaded programs where all threads but
+        one are known to be stopped (as they are when the debugger is
+        decoding the call stack in the use case described above).
+
+
 .. c:function:: mps_bool_t mps_arena_has_addr(mps_arena_t arena, mps_addr_t addr)
 
     Test whether an :term:`address` is managed by an :term:`arena`.