- //@DeclareStruct:
- //typedef struct elem {
- // t_element *pos;
- // bool written;
- // thread_id_t tid;
- // thread_id_t fetch_tid;
- // call_id_t id;
- // } elem;
- // @DeclareVar:
- // spec_list *list;
- //id_tag_t *tag;
- // @InitVar:
- // list = new_spec_list();
- //tag = new_id_tag();
- // @Cleanup:
-// if (list)
-// free_spec_list();
- @Happens_before:
- Publish -> Fetch
- Consume -> Prepare
+ @Happens_before:
+ Publish -> Fetch
+ Consume -> Prepare
+ @Commutativity: Prepare <-> Prepare: _Method1.__RET__ !=
+ _Method2.__RET__ || !_Method1.__RET__ || !_Method2.__RET__
+ @Commutativity: Prepare <-> Publish: _Method1.__RET__ != _Method2.bin ||
+ !_Method1.__RET__
+ @Commutativity: Prepare <-> Fetch: _Method1.__RET__ != _Method2.__RET__
+ || !_Method1.__RET__ || !_Method2.__RET__
+ @Commutativity: Prepare <-> Consume : _Method1.__RET__ != _Method2.bin || !_Method1.__RET__
+
+ @Commutativity: Publish <-> Publish: _Method1.bin != _Method2.bin
+ @Commutativity: Publish <-> Fetch: _Method1.bin != _Method2.__RET__ ||
+ !_Method2.__RET__
+ @Commutativity: Publish <-> Consume : _Method1.bin != _Method2.bin
+
+ @Commutativity: Fetch <-> Fetch: _Method1.__RET__ != _Method2.__RET__ ||
+ !_Method1.__RET__ || !_Method2.__RET__
+ @Commutativity: Fetch <-> Consume : _Method1.__RET__ != _Method2.bin || !_Method1.__RET__
+
+ @Commutativity: Consume <-> Consume : _Method1.bin != _Method2.bin
+