Add a new section for putting global codes (phase 1)
Add a new section for putting global codes (phase 2)
Use a monomorphic function instead of the polymorphic operator <>
Fix issues with lists reversed
More work on c/cpp generators.
The new -check true mode should avoid spurious data races
Consider for instance MP+ponarel+poacqna that is racy
with -check false and is not with -check true,
as the second load (value) is performed only when the first load
(flag) reads the value 1.
Resolved conflict by hand-merging

Merge branch 'master' of github.com:herd/herdtools

Conflicts:
	litmus/top.ml
New out-of-thin-air test.
Correct threads  count for the C arch
Add non-initialised globals in typing envinronment.
When a register or global is initialised with the global address.
This is mandatory for instructing litmus to consider those globals.
The type defaults to int.
Avoid a few warnings.
Add get_addr to C templates: this function returns the globals
referenced by a given proc code (in practice, arguments).

Also, suppress intermediate variables x,y,... (= _a->x, _a->y etc.)
in machine arch case
Tag p -> na for plain accesses in namer.
Neatened up code.
Added a couple of explanatory comments.
Lots of changes. CPP11 is now properly incorporated into Herd, in
what I hope is a pleasingly modular way. Most significant changes
are as follows:

- Each architecture defines some special sets that will be available
  in every model, e.g. CPP11 defines "rmw" as the set of RMW events.

- CPP11 no longer uses the Barrier and Commit actions. Instead of
  Barrier, it defines its own Fence action. (I found that trying to
  use the machinery for hardware barriers in the CPP11 model was
  quite cumbersome.) As a consequence, CPP11 fences no longer feature
  in the list of all barriers.

- I split Generic into an Interpreter and two "model checkers", which
  both use the Interpreter. The MachModelChecker is for machine
  memory models, and the CPP11ModelChecker is for CPP11. The latter
  includes the "lo" (lock-order) relation, which is generated by the
  new "apply_process_lo" function in MemUtils.

- I made the event monad slightly more generic. The mk_singleton_es
  function now supersedes the previous create_barrier, commit, and
  write_loc functions. You just pass it an action, and it makes you
  a singleton event structure. As an unfortunate consequence, there
  is now a bit more repetition between ARMSem, PPCSem and X86Sem,
  which I'm not really sure how to remove.

- The value type in the Interpreter is extended to include sets, as
  well as relations and closures. As a result, I added "set" and
  "rln" as new keywords.

- I added "provides" and "requires" as new keywords. One uses
  "requires" clauses to create undefinedness in models -- this is
  relevant for language-level memory models. The implementation
  doesn't do anything yet -- I still need to move this over from
  the cpp+gpu branch.
Minor
Merge commit 'dcae1a5603bdba3243ba88d210803f6a686e835b' into cpp