1. Template support
  The global specification should be expanded right after the specification
  definition (the golbal construct). The global variables and functions will be
  the private members of the data structure. In this case, the template of the
  data structure can be automatically passed to the variables and functions.
  Besides, as the public member of the function, all the interface check can
  access the specification variables and functions just as normal.

2. On-the-fly spec check
  For a check and action, they will be expanded right at the place where they
  are declared and will get executed when the inserted annotation gets executed.
  And the annotation is just a way to pass if the checks are satisfied. However,
  it is wrong because the annotation is also a type of atomic operation. For
  example, for a potential commit point and a later commit point check, they
  might be interleaved by another commit point. Therefore, we need to check in
  the specanalysis to see if the specific interleaving of annotation is "legal".

3. Happens-before initialization
  This concerns the place where we pass to the specanalysis the happens-before
  rules????