edits

diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
index 9195e13a6c70a479d44ade76a9d27658de8299a2..2a8c779d07e5e34e34f05c2e6eadefa763b5e097 100644 (file)
--- a/grammer/spec_compiler.jj
+++ b/grammer/spec_compiler.jj
@@ -9,129 +9,52 @@
        annotation would be considered as normal comments of the source.
        
        a) Global construct
-       @Begin
-       @Options:
-               # If LANG is not define, it's C++ by default. C does not support class
-               # and template, so if it's defined as C, we should also have a explicit
-               # entry point.
-               LANG = C;
-       @Global_define:
-               @DeclareStruct:
-               @DeclareVar:
-               @InitVar:
-               @DefineFunc:
-               ...
-               @DefineFunc:
-       @Interface_cluster:
-               ...
-       @Happens_before:
-               ...
-       @Commutativity: // This is to define the admissibility condition
-               // Enq <-> Enq (_M1.q != _M2.q)
-               // Enq <-> Deq (_M1.q != _M2.q)
-               // Deq <-> Deq (_M1.q != _M2.q)
-               // Enq <-> Deq (_M1.q == _M2.q && _M2.__RET__ == NULL)
-       @End
+       @DeclareState: C/C++ variable declaration; // Declare the state structure
+       @InitState: C/C++ statements; // Specify how to initialize the state
+       @CopyState: // A function on how to copy an existing state (Not sure if we
+                               // need this because we might be able to auto this
+       @Commutativity: Method1 <-> Method2 (Guard) // Admissibility condition.
+                                                                                               // Allow specify 0-many rules
        
        b) Interface construct
-       @Begin
-       @Interface_decl: ...
-       @Commit_point_set:
-               IDENTIFIER | IDENTIFIER ...
-       @Condition: ... (Optional)
-       @HB_Condition:
-               IDENTIFIER :: <C_CPP_Condition>
-       @HB_Condition: ...
-       @ID: ... (Optional, use default ID)
-       @Check: (Optional)
-               ...
-       @Action: (Optional)
-               ...
-       @Post_action: (Optional)
-       @Post_check: (Optional)
-       @End
-
-       c) Potential commit construct
-       @Begin
-       @Potential_commit_point_define: ...
-       @Label: ...
-       @End
-
-               OR
-
-       @Begin
-       @Potential_additional_ordering_point_define: ...
-       @Label: ...
-       @End
-
-       d) Commit point define construct
-       @Begin
-       @Commit_point_define_check: ...
-       @Label: ...
-       @End
-
-               OR
-       
-       # Addition ordering point is used to order operations when there are "equal"
-       # commit point operations on the same location and that we cannot decide
-       # which operation goes first, we will use additional ordering point to order
-       # them (it's just similar to commit points). In implementation, we can just
-       # treat them as commit points with a special flag.
-
-       @Begin
-       @Additional_ordering_point_define: ...
-       @Potential_additional_ordering_point_label: ...
-       @Label: ...
-       @End
-       
-               OR
-       
-       @Begin
-       @Additional_ordering_point_define: ...
-       @Label: ...
-       @End
-
-               OR
-
-       @Begin
-       @Additional_ordering_point_define_check: ...
-       @Label: ...
-       @End
-
-       // Commit point clear (just as a normal commit point, but it is used to
-       // clear all commit points)
-       @Begin
-       @Commit_point_clear: ...
-       @Label: ...
-       @End
-
-       e) Entry point construct
-       @Begin
-       @Entry_point
-       @End
-
-       f) Interface define construct
-       @Begin
-       @Interface_define: <Interface_Name>
-       @End
-
-       g) Interface declare & define construct
-       @Begin
-       @Interface_decl_define: <Interface_Name>
-       @Commit_point_set:
-               IDENTIFIER | IDENTIFIER ...
-       @Condition: ... (Optional)
-       @HB_Condition:
-               IDENTIFIER :: <C_CPP_Condition>
-       @HB_Condition: ...
-       @ID: ... (Optional, use default ID)
-       @Check: (Optional)
-               ...
-       @Action: (Optional)
-               ...
-       @Post_action: (Optional)
-       @Post_check: (Optional)
-       @End
+       @Interface: InterfaceName // Required; a label to represent the interface
+       @LocalState: // Optional; to calculate the accumulative local state before this
+                                // method call in a customized fashion. If not specified here, the
+                                // local state would be default, which is the result of the
+                                // execution on the subset of method calls in the sequential order
+       @PreCondition: // Optional; checking code
+       @LocalSideEffect: // Optional; to calculate the side effect this method call
+                                         // have on the local state in a customized fashion. If this
+                                         // field is not stated, it means we don't care about it.
+       @SideEffect: // Optional; to calculate the side effect on the global state. When
+                       // the "@LocalSideEffect" specification is ommitted, we also impose the
+                       // same side effect on the set of method calls that happen before this
+                       // method call in the sequential order.
+       @PostCondition: // Optional; checking code
+
+
+       c) Ordering point construct
+       @OPDefine: condition    // If the specified condition satisfied, the atomic
+                                                       // operation right before is an ordering point
+
+       @PotentialOP(Label): condition  // If the specified condition satisfied, the
+                                                                       // atomic operation right before is a potential
+                                                                       // ordering point, and we label it with a tag
+
+       @OPCheck(Label): condition      // If the specified condition satisfied, the
+                                                               // potential ordering point defined earlier with the
+                                                               // same tag becomes an ordering point
+
+       @OPClear: condition             // If the specified condition satisfied, all the
+                                                       // ordering points and potential ordering points will be
+                                                       // cleared
+
+       @OPClearDefine: condition       // If the specified condition satisfied, all the
+                                                               // ordering points and potential ordering points will
+                                                               // be cleared, and the atomic operation right before
+                                                               // becomes an ordering point. This is a syntax sugar
+                                                               // as the combination of an "OPClear" and "OPDefine"
+                                                               // statement
 
 */