+
+ /**
+ @Begin
+ @Options:
+ LANG = CPP;
+ CLASS = spsc_queue;
+ @Global_define:
+ @DeclareStruct:
+ typedef struct tag_elem {
+ call_id_t id;
+ T data;
+ } tag_elem_t;
+
+ @DeclareVar:
+ spec_list *__queue;
+ id_tag_t *tag;
+ @InitVar:
+ __queue = new_spec_list();
+ tag = new_id_tag();
+ @DefineFunc:
+ tag_elem_t* new_tag_elem(call_id_t id, T data) {
+ tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
+ e->id = id;
+ e->data = data;
+ return e;
+ }
+ @DefineFunc:
+ call_id_t get_id(void *wrapper) {
+ return ((tag_elem_t*) wrapper)->id;
+ }
+ @DefineFunc:
+ unsigned int get_data(void *wrapper) {
+ return ((tag_elem_t*) wrapper)->data;
+ }
+ @Happens_before:
+ Enqueue -> Dequeue
+ @End
+ */
+