+ list = new_spec_list();
+ tag = new_id_tag();
+ @DefineFunc:
+ elem* new_elem(t_element *pos, call_id_t id, thread_id_t tid) {
+ elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
+ e->pos = pos;
+ e->written = false;
+ e->id = id;
+ e->tid = tid;
+ e->fetch_tid = -1;
+ }
+ @DefineFunc:
+ elem* get_elem_by_pos(t_element *pos) {
+ for (int i = 0; i < size(list); i++) {
+ elem *e = (elem*) elem_at_index(list, i);
+ if (e->pos == pos) {
+ return e;
+ }
+ }
+ return NULL;
+ }
+ @DefineFunc:
+ void show_list() {
+ //model_print("Status:\n");
+ for (int i = 0; i < size(list); i++) {
+ elem *e = (elem*) elem_at_index(list, i);
+ //model_print("%d: pos %d, written %d, tid %d, fetch_tid %d, call_id %d\n", i, e->pos, e->written, e->tid, e->fetch_tid, e->id);
+ }
+ }
+ @DefineFunc:
+ elem* get_elem_by_tid(thread_id_t tid) {
+ for (int i = 0; i < size(list); i++) {
+ elem *e = (elem*) elem_at_index(list, i);
+ if (e->tid== tid) {
+ return e;
+ }
+ }
+ return NULL;
+ }
+ @DefineFunc:
+ elem* get_elem_by_fetch_tid(thread_id_t fetch_tid) {
+ for (int i = 0; i < size(list); i++) {
+ elem *e = (elem*) elem_at_index(list, i);
+ if (e->fetch_tid== fetch_tid) {
+ return e;
+ }
+ }
+ return NULL;
+ }
+ @DefineFunc:
+ int elem_idx_by_pos(t_element *pos) {
+ for (int i = 0; i < size(list); i++) {
+ elem *existing = (elem*) elem_at_index(list, i);
+ if (pos == existing->pos) {
+ return i;
+ }
+ }
+ return -1;
+ }
+ @DefineFunc:
+ int elem_idx_by_tid(thread_id_t tid) {
+ for (int i = 0; i < size(list); i++) {
+ elem *existing = (elem*) elem_at_index(list, i);
+ if (tid == existing->tid) {
+ return i;
+ }
+ }
+ return -1;
+ }
+ @DefineFunc:
+ int elem_idx_by_fetch_tid(thread_id_t fetch_tid) {
+ for (int i = 0; i < size(list); i++) {
+ elem *existing = (elem*) elem_at_index(list, i);
+ if (fetch_tid == existing->fetch_tid) {
+ return i;
+ }
+ }
+ return -1;
+ }
+ @DefineFunc:
+ int elem_num(t_element *pos) {
+ int cnt = 0;
+ for (int i = 0; i < size(list); i++) {
+ elem *existing = (elem*) elem_at_index(list, i);
+ if (pos == existing->pos) {
+ cnt++;
+ }
+ }
+ return cnt;
+ }
+ @DefineFunc:
+ call_id_t prepare_id() {
+ call_id_t res = get_and_inc(tag);
+ //model_print("prepare_id: %d\n", res);
+ return res;
+ }
+ @DefineFunc:
+ bool prepare_check(t_element *pos, thread_id_t tid) {
+ show_list();
+ elem *e = get_elem_by_pos(pos);
+ //model_print("prepare_check: e %d\n", e);
+ return NULL == e;
+ }
+ @DefineFunc:
+ void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
+ //model_print("prepare: id %d, pos %d, tid %d\n", id, pos, tid);
+ elem *e = new_elem(pos, id, tid);
+ push_back(list, e);
+ }
+ @DefineFunc:
+ call_id_t publish_id(thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ //model_print("publish_id: id %d\n", e == NULL ? 0 : e->id);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ bool publish_check(thread_id_t tid) {
+ show_list();
+ elem *e = get_elem_by_tid(tid);
+ //model_print("publish_check: tid %d\n", tid);
+ if (NULL == e)
+ return false;
+ if (elem_num(e->pos) > 1)
+ return false;
+ return !e->written;
+ }
+ @DefineFunc:
+ void publish(thread_id_t tid) {
+ //model_print("publish: tid %d\n", tid);
+ elem *e = get_elem_by_tid(tid);
+ e->written = true;
+ }
+ @DefineFunc:
+ call_id_t fetch_id(t_element *pos) {
+ elem *e = get_elem_by_pos(pos);
+ //model_print("fetch_id: id %d\n", e == NULL ? 0 : e->id);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ bool fetch_check(t_element *pos) {
+ show_list();
+ if (pos == NULL) return true;
+ elem *e = get_elem_by_pos(pos);
+ //model_print("fetch_check: pos %d, e %d\n", pos, e);
+ if (e == NULL) return false;
+ if (elem_num(e->pos) > 1)
+ return false;
+ return true;
+ }
+ @DefineFunc:
+ void fetch(t_element *pos, thread_id_t tid) {
+ if (pos == NULL) return;
+ elem *e = (elem*) get_elem_by_pos(pos);
+ //model_print("fetch: pos %d, tid %d\n", pos, tid);
+ // Remember the thread that fetches the position
+ e->fetch_tid = tid;
+ }
+ @DefineFunc:
+ bool consume_check(thread_id_t tid) {
+ show_list();
+ elem *e = get_elem_by_fetch_tid(tid);
+ //model_print("consume_check: tid %d, e %d\n", tid, e);
+ if (NULL == e)
+ return false;
+ if (elem_num(e->pos) > 1)
+ return false;
+ return e->written;
+ }
+ @DefineFunc:
+ call_id_t consume_id(thread_id_t tid) {
+ elem *e = get_elem_by_fetch_tid(tid);
+ //model_print("consume_id: id %d\n", e == NULL ? 0 : e->id);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ void consume(thread_id_t tid) {
+ //model_print("consume: tid %d\n", tid);
+ int idx = elem_idx_by_fetch_tid(tid);
+ if (idx == -1)
+ return;
+ remove_at_index(list, idx);
+ }