Methodology for using DeterministicSchedule support for auxiliary data and global...

Methodology for using DeterministicSchedule support for auxiliary data and global invariants

Summary:
Depends on D3648195

This test example is intended to demonstrate the methodology for using DeterministicSchedule support for auxiliary data and global invariants.
The main goal is fine-grained invariant checking, ideally after every shared update.
The secondary goals are:
- Minimize intrusion in the original code. In this proposed methodology, it is adding a friend.
- Minimize duplication of original tested code. Unfortunately, depending on the original code, it seems that significant duplication may be unavoidable if we don't want to change the original code.

This diff is primarily about the methodology for testing already developed code. I plan to apply what we agree on through this diff to the dynamic MPMCQueue code (D3462592).

A future goal to keep in mind is creating a methodology for developing new code with hooks for DSched aux. data and invariant checking integrated in it, in order to minimize or eliminate duplication of tested code.  In past projects, I used non-standard source code (basically algorithm code) that is automatically translatable through scripts and macros to input to a DSched-like tool as well as to compilable code. The main challenge for such a methodology is to allow the original source code to be standard readable C++ code.

Reviewed By: djwatson

Differential Revision: D3675447

fbshipit-source-id: aae2c9f0550af88dc3a5dcbe53318a75a86b6e2b