notes/impl.txt

   1 1. Template support
   2   The global specification should be expanded right after the specification
   3   definition (the golbal construct). The global variables and functions will be
   4   the private members of the data structure. In this case, the template of the
   5   data structure can be automatically passed to the variables and functions.
   6   Besides, as the public member of the function, all the interface check can
   7   access the specification variables and functions just as normal.
   8
   9 2. On-the-fly spec check
  10   For a check and action, they will be expanded right at the place where they
  11   are declared and will get executed when the inserted annotation gets executed.
  12   And the annotation is just a way to pass if the checks are satisfied. However,
  13   it is wrong because the annotation is also a type of atomic operation. For
  14   example, for a potential commit point and a later commit point check, they
  15   might be interleaved by another commit point. Therefore, we need to check in
  16   the specanalysis to see if the specific interleaving of annotation is "legal".
  17
  18 3. Happens-before initialization
  19   This concerns the place where we pass to the specanalysis the happens-before
  20   rules????
  21
  22 4. To make implementation easier and the spec cleaner, we make a difference C
  23   and C++ programs. Since C does not support template and class, we require
  24   users to provide an entry point where we can initialize the sequential
  25   variables. By default, it's a C++ program, and everything is wrapped in an
  26   inner class because it can have easy initialization and template support.
  27
  28 5. We add @Interface_define construct in the specification. Basically,
  29   @Interface construct can be used in both interface declaration and interface
  30   definition, if they are not separated. However, if they are, then @Interface
  31   is used for the interface declaration and @Interface_define is for the
  32   interface definition. This is redundant information, but it makes the
  33   implementation much easier because we don't need to parse the C/C++ program.
  34
  35 6. Checking at runtime or check with complete trace analysis can have the
  36   follwing concerns. Checking at runtime, HB might not be established yet (we
  37   can leave it at trace analysis though). More importantly, we have potential
  38   commit point and commit point check, which might be preempted by another
  39   commit point. We can't decide whether to execute the commit point actions or
  40   not since we can't decide if it's really a commit point at that time. Checking
  41   with complete execution can be more clear and better designed, but it has a
  42   tough challenge. Some data structure may check their predicate with pointers,
  43   however, we can't guarantee those pointers are still valid (the object they
  44   are pointing to may be changed or even deleted). To tackle this, we provide an
  45   alternative which requires users to define the snapshot function for the
  46   pointers if they are about to check with pointers that might change. In the
  47   current data structure, it's not a problem because they only return reference
  48   or pointers, which we can do simple equality check. We decided to take the
  49   trace analysis approach because it's still more flexible and easier to
  50   implement.