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.
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".
18 3. Happens-before initialization
19 This concerns the place where we pass to the specanalysis the happens-before
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.
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.