void ReleaseBuffer(Buffer buf)

• decrement pin count on buffer
• if pin count falls to zero,
  ensures all activity on buffer is completed before returning

• marks a buffer as modified
• requires that buffer is pinned and locked
• actual write is done later (e.g. when buffer replaced)