Res EventInit(void)
{
  Res res;

  /* Only if this is the first call. */
  if(!eventInited) { /* See .trans.log */
    AVER(EventNext == 0);
    AVER(EventLimit == 0);
    res = (Res)mps_io_create(&eventIO);
    if(res != ResOK) return res;
    EventNext = eventBuffer;
    EventLimit = &eventBuffer[EventBufferSIZE];
    eventUserCount = (Count)1;
    eventError = ResOK;
    eventInited = TRUE;
    EventKindControl = (Word)mps_lib_telemetry_control();
    EventInternSerial = (Serial)1; /* 0 is reserved */
    (void)EventInternString(MPSVersion()); /* emit version */
  } else {
    ++eventUserCount;
  }

  return ResOK;
}

static void mapThreadRing(Ring threadRing, void (*func)(Thread))
{
  Ring node, next;
  mach_port_t self;

  AVERT(Ring, threadRing);

  self = mach_thread_self();
  AVER(MACH_PORT_VALID(self));
  RING_FOR(node, threadRing, next) {
    Thread thread = RING_ELT(Thread, arenaRing, node);
    AVERT(Thread, thread);
    if(thread->port != self)
      (*func)(thread);
  }

void TreeRotateLeft(Tree *treeIO)
{
  Tree tree, right;

  AVER(treeIO != NULL);
  tree = *treeIO;
  AVERT(Tree, tree);
  right = TreeRight(tree);
  AVERT(Tree, right);

  TreeSetRight(tree, TreeLeft(right));
  TreeSetLeft(right, tree);

  *treeIO = right;
}

void VMDestroy(VM vm)
{
  int r;
  int zero_fd;

  AVERT(VM, vm);
  AVER(vm->mapped == (Size)0);

  /* This appears to be pretty pointless, since the descriptor */
  /* page is about to vanish completely.  However, munmap might fail */
  /* for some reason, and this would ensure that it was still */
  /* discovered if sigs were being checked. */
  vm->sig = SigInvalid;

  zero_fd = vm->zero_fd;
  r = munmap((void *)vm->base, (size_t)AddrOffset(vm->base, vm->limit));
  AVER(r == 0);
  r = munmap((void *)vm, (size_t)SizeAlignUp(sizeof(VMStruct), vm->align));
  AVER(r == 0);
  r = close(zero_fd);
  AVER(r == 0);

  EVENT_P(VMDestroy, vm);
}

Res BufferReserve(Addr *pReturn, Buffer buffer, Size size)
{
  Addr next;

  AVER(pReturn != NULL);
  AVERT(Buffer, buffer);
  AVER(size > 0);
  AVER(SizeIsAligned(size, BufferPool(buffer)->alignment));
  AVER(BufferIsReady(buffer)); /* <design/check/#.common> */

  /* Is there enough room in the unallocated portion of the buffer to */
  /* satisfy the request?  If so, just increase the alloc marker and */
  /* return a pointer to the area below it. */
  next = AddrAdd(buffer->ap_s.alloc, size);
  if (next > (Addr)buffer->ap_s.alloc &&
      next <= (Addr)buffer->ap_s.limit) {
    buffer->ap_s.alloc = next;
    *pReturn = buffer->ap_s.init;
    return ResOK;
  }

  /* If the buffer can't accommodate the request, call "fill". */
  return BufferFill(pReturn, buffer, size);
}

static void vmArenaUnmap(VMArena vmArena, VM vm, Addr base, Addr limit)
{
  Arena arena;
  Size size;

  /* no checking as function is local to module */

  arena = VMArena2Arena(vmArena);
  size = AddrOffset(base, limit);
  AVER(size <= arena->committed);

  VMUnmap(vm, base, limit);
  arena->committed -= size;
  return;
}

void (ShieldRaise) (Arena arena, Seg seg, AccessSet mode)
{
    /* .seg.broken: Seg's shield invariants may not be true at */
    /* this point (this function is called to enforce them) so we */
    /* can't check seg. Nor can we check arena as that checks the */
    /* segs in the cache. */

    AVER((SegSM(seg) & mode) == AccessSetEMPTY);
    SegSetSM(seg, SegSM(seg) | mode); /* inv.prot.shield preserved */

    /* ensure inv.unsynced.suspended & inv.unsynced.depth */
    cache(arena, seg);
    AVERT(Arena, arena);
    AVERT(Seg, seg);
}

void mps_pool_check_fenceposts(mps_pool_t mps_pool)
{
  Pool pool = (Pool)mps_pool;
  Arena arena;
  
  /* TESTT not AVERT, see <design/interface-c/#check.space */
  AVER(TESTT(Pool, pool));
  arena = PoolArena(pool);

  ArenaEnter(arena);

  AVERT(Pool, pool);
  DebugPoolCheckFences(pool);

  ArenaLeave(arena);
}

Res StackScan(ScanState ss, Addr *stackBot)
{
  jmp_buf jb;
  void *stackTop = &jb;

  /* .assume.stack: This implementation assumes that the stack grows
   * downwards, so that the address of the jmp_buf is the limit of the
   * part of the stack that needs to be scanned. (StackScanInner makes
   * the same assumption.)
   */
  AVER(stackTop < (void *)stackBot);

  (void)setjmp(jb);

  return StackScanInner(ss, stackBot, stackTop, sizeof jb / sizeof(Addr*));
}

static void BufferAbsFinish(Inst inst)
{
  Buffer buffer = MustBeA(Buffer, inst);
  AVERT(Buffer, buffer);
  AVER(BufferIsReset(buffer));

  /* Detach the buffer from its owning pool and unsig it. */
  RingRemove(&buffer->poolRing);
  InstFinish(MustBeA(Inst, buffer));
  buffer->sig = SigInvalid;
 
  /* Finish off the generic buffer fields. */
  RingFinish(&buffer->poolRing);

  EVENT1(BufferFinish, buffer);
}

Res MutatorContextScan(ScanState ss, MutatorContext context,
                       mps_area_scan_t scan_area, void *closure)
{
  CONTEXT *cx;
  Res res;

  AVERT(ScanState, ss);
  AVERT(MutatorContext, context);
  AVER(context->var == MutatorContextTHREAD);

  cx = &context->the.context;
  res = TraceScanArea(ss, (Word *)cx, (Word *)((char *)cx + sizeof *cx),
                      scan_area, closure); /* .context.regroots */

  return res;
}

void mps_pool_check_free_space(mps_pool_t mps_pool)
{
  Pool pool = (Pool)mps_pool;
  Arena arena;
  
  /* TESTT not AVERT, see <design/interface-c#.check.space */
  AVER(TESTT(Pool, pool));
  arena = PoolArena(pool);

  ArenaEnter(arena);

  AVERT(Pool, pool);
  DebugPoolCheckFreeSpace(pool);

  ArenaLeave(arena);
}

/* LDReset -- reset a dependency to empty
 *
 * .reset.sync: This does not need to be synchronized with LDAge
 * because if the epoch advances after it is read the dependency
 * will simply include movement for more time than necessary.
 */
void LDReset(mps_ld_t ld, Arena arena)
{
  Bool b;
  Seg seg;

  AVER(ld != NULL);
  AVERT(Arena, arena);

  b = SegOfAddr(&seg, arena, (Addr)ld);
  if (b)
    ShieldExpose(arena, seg);   /* .ld.access */
  ld->_epoch = arena->epoch;
  ld->_rs = RefSetEMPTY;
  if (b)
    ShieldCover(arena, seg);
}

Count TreeToVine(Tree *link)
{
  Count count = 0;
  
  AVER(link != NULL);
  AVERT(Tree, *link);

  while (*link != TreeEMPTY) {
    while (TreeHasLeft(*link))
      TreeRotateRight(link);
    link = &((*link)->right);
    ++count;
  }
  
  return count;
}

static Res MVFFAlloc(Addr *aReturn, Pool pool, Size size,
                     Bool withReservoirPermit)
{
  Res res;
  MVFF mvff;
  Addr base, limit;
  Bool foundBlock;

  AVERT(Pool, pool);
  mvff = Pool2MVFF(pool);
  AVERT(MVFF, mvff);

  AVER(aReturn != NULL);
  AVER(size > 0);
  AVERT(Bool, withReservoirPermit);

  size = SizeAlignUp(size, PoolAlignment(pool));

  foundBlock = MVFFFindFirstFree(&base, &limit, mvff, size);
  if (!foundBlock) {
    Seg seg;

    res = MVFFAddSeg(&seg, mvff, size, withReservoirPermit);
    if (res != ResOK)
      return res;
    foundBlock = MVFFFindFirstFree(&base, &limit, mvff, size);

    /* We know that the found range must intersect the new segment. */
    /* In particular, it doesn't necessarily lie entirely within it. */
    /* The next three AVERs test for intersection of two intervals. */
    AVER(base >= SegBase(seg) || limit <= SegLimit(seg));
    AVER(base < SegLimit(seg));
    AVER(SegBase(seg) < limit);

    /* We also know that the found range is no larger than the segment. */
    AVER(SegSize(seg) >= AddrOffset(base, limit));
  }
  AVER(foundBlock);
  AVER(AddrOffset(base, limit) == size);

  *aReturn = base;

  return ResOK;
}

static Res MFSInit(Pool pool, ArgList args)
{
  Size extendBy = MFS_EXTEND_BY_DEFAULT;
  Bool extendSelf = TRUE;
  Size unitSize;
  MFS mfs;
  Arena arena;
  ArgStruct arg;

  AVER(pool != NULL);
  AVERT(ArgList, args);
  
  ArgRequire(&arg, args, MPS_KEY_MFS_UNIT_SIZE);
  unitSize = arg.val.size;
  if (ArgPick(&arg, args, MPS_KEY_EXTEND_BY))
    extendBy = arg.val.size;
  if (ArgPick(&arg, args, MFSExtendSelf))
    extendSelf = arg.val.b;

  AVERT(Bool, extendSelf);
 
  mfs = PoolPoolMFS(pool);
  arena = PoolArena(pool);

  mfs->unroundedUnitSize = unitSize;

  if (unitSize < UNIT_MIN)
    unitSize = UNIT_MIN;
  unitSize = SizeAlignUp(unitSize, MPS_PF_ALIGN);
  if (extendBy < unitSize)
    extendBy = unitSize;
  extendBy = SizeArenaGrains(extendBy, arena);

  mfs->extendBy = extendBy;
  mfs->extendSelf = extendSelf;
  mfs->unitSize = unitSize;
  mfs->freeList = NULL;
  mfs->tractList = NULL;
  mfs->total = 0;
  mfs->free = 0;
  mfs->sig = MFSSig;

  AVERT(MFS, mfs);
  EVENT5(PoolInitMFS, pool, arena, extendBy, BOOLOF(extendSelf), unitSize);
  return ResOK;
}

static void MVFFFinish(Pool pool)
{
  MVFF mvff;
  Arena arena;
  Seg seg;
  Ring ring, node, nextNode;

  AVERT(Pool, pool);
  mvff = Pool2MVFF(pool);
  AVERT(MVFF, mvff);

  ring = PoolSegRing(pool);
  RING_FOR(node, ring, nextNode) {
    seg = SegOfPoolRing(node);
    AVER(SegPool(seg) == pool);
    SegFree(seg);
  }

Res BufferFramePush(AllocFrame *frameReturn, Buffer buffer)
{
  Pool pool;
  AVERT(Buffer, buffer);
  AVER(frameReturn != NULL);


  /* Process any flip */
  if (!BufferIsReset(buffer) && buffer->ap_s.limit == (Addr)0) {
    /* .fill.unflip: If the buffer is flipped then we unflip the buffer. */
    if (buffer->mode & BufferModeFLIPPED) {
      BufferSetUnflipped(buffer);
    }
  }
  pool = BufferPool(buffer);
  return Method(Pool, pool, framePush)(frameReturn, pool, buffer);
}

static void SplayLinkLeft(SplayNode *topIO, SplayNode *leftIO) {
    AVERT(SplayNode, *topIO);
    AVERT(SplayNode, *leftIO);

    /* Don't fix client properties yet. */

    /* .link.left.first: *leftIO is always the last node in the */
    /* left tree, so its right child must be null. */
    AVER(SplayNodeRightChild(*leftIO) == NULL);

    SplayNodeSetRightChild(*leftIO, *topIO);
    *leftIO = *topIO;
    *topIO = SplayNodeRightChild(*topIO);

    /* The following line is only required for .link.left.first. */
    SplayNodeSetRightChild(*leftIO, NULL);
}

static void SplayAssembleRev(SplayTree splay, SplayState state)
{
  Tree left, right;

  AVERT(SplayTree, splay);
  AVER(state->middle != TreeEMPTY);
  
  left = TreeLeft(state->middle);
  left = SplayUpdateRightSpine(splay, state->leftLast, left);
  TreeSetLeft(state->middle, left);

  right = TreeRight(state->middle);
  right = SplayUpdateLeftSpine(splay, state->rightFirst, right);
  TreeSetRight(state->middle, right);

  splay->updateNode(splay, state->middle);
}