@Override
  public synchronized void flush() throws IOException {
    if (MARK_SAFELY_CLOSED_ON_FLUSH) {
      //RC: Since EHMap is non-concurrent (sync-ed), it seems safe to set .fileStatus(PROPERLY_CLOSED) in
      //    .flush(): nobody could modify EHMap content until .flush() finishes, which creates kind of
      //    'safepoint'.
      //    (On the contrary: data structures with concurrent updates don't have this property: their
      //    content could be modified in between .flush() sets .dirty=false and .fileStatus=PROPERLY_CLOSED)

      if (dirty) {
        dirty = false;
        header.fileStatus(HeaderLayout.FILE_STATUS_PROPERLY_CLOSED);
      }
    }
  }
@Override
  public synchronized void flush()