From 37a6bc832e220afbfb100848da62fb1b2123af63 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 28 Jan 2016 18:07:22 -0800 Subject: [PATCH] edits --- grammer/spec_compiler.jj | 165 +++++++++++---------------------------- 1 file changed, 44 insertions(+), 121 deletions(-) diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 9195e13..2a8c779 100644 --- 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 :: - @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: - @End - - g) Interface declare & define construct - @Begin - @Interface_decl_define: - @Commit_point_set: - IDENTIFIER | IDENTIFIER ... - @Condition: ... (Optional) - @HB_Condition: - IDENTIFIER :: - @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 */ -- 2.34.1