@DefineFunc:
@Interface_cluster:
...
- @Happens-before:
+ @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
b) Interface construct
import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CommutativityRule;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
<INTERFACE_CLUSTER: "@Interface_cluster:">
|
<HAPPENS_BEFORE: "@Happens_before:">
+|
+ <COMMUTATIVITY: "@Commutativity:">
|
<INTERFACE: "@Interface:">
|
<CLOSE_BRACE: "}">
|
<HB_SYMBOL: "->">
+|
+ <COMMUTATIVITY_SYMBOL: "<->">
|
<COMMA: ",">
|
{ res = new GlobalConstruct(_file, _content.size(), code, options); }
(Interface_clusters(res))?
(Happens_before(res))?
+ (Commutativity(res))?
<END>
{
res.unfoldInterfaceCluster();
)+
}
+void Commutativity(GlobalConstruct inst) :
+{
+ String method1, method2, condition;
+ ArrayList<String> content;
+}
+{
+ {
+ content = new ArrayList<String>();
+ }
+
+ (
+ <COMMUTATIVITY>
+ method1 = <IDENTIFIER>.image <COMMUTATIVITY_SYMBOL>
+ method2 = <IDENTIFIER>.image
+ <COLON>
+ content = C_CPP_CODE(null)
+ { condition = stringArray2String(content); }
+ {
+ inst.addCommutativityRule(method1, method2, condition);
+ }
+ )+
+}
+
InterfaceConstruct Interface() :
{
InterfaceConstruct res;