CLASS = mpmc_boundq_1_alt;
@DeclareStruct:
typedef struct elem {
- t_element* pos;
+ t_element *pos;
boolean written;
+ thread_id_t tid;
call_id_t id;
} elem;
@DeclareVar:
list = new_spec_list();
tag = new_id_tag();
@DefineFunc:
- elem* new_elem(t_element *pos, call_id_t id) {
+ 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;
}
@DefineFunc:
- elem* get_elem(t_element *pos) {
+ 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 NULL;
}
@DefineFunc:
- int has_elem(t_element *pos) {
+ 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:
+ 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 -1;
}
@DefineFunc:
- void prepare(t_element *pos) {
- elem *e = new_elem(
- push_back(list, e);
+ 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:
+ call_id_t prepare_id() {
+ return get_and_inc(tag);
+ }
+ @DefineFunc:
+ bool prepare_check(t_element *pos, thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ return NULL == e;
}
@DefineFunc:
- void publish(t_element *pos) {
- elem *e = new_elem(
+ void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
+ call_id_t id = get_and_inc(tag);
+ elem *e = new_elem(pos, id, tid);
push_back(list, e);
}
@DefineFunc:
- void consume_elem(t_element *pos) {
- int idx = has_elem(pos);
+ call_id_t publish_id(thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ bool publish_check(thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ if (NULL == e)
+ return false;
+ return e->written;
+ }
+ @DefineFunc:
+ void publish(thread_id_t 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);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ bool fetch_check(t_element *pos) {
+ int idx = elem_idx_by_pos(pos);
+ if (idx == -1)
+ return false;
+ else
+ return true;
+ }
+ @DefineFunc:
+ void fetch(t_element *pos) {
+ int idx = elem_idx_by_pos(pos);
if (idx == -1)
return;
remove_at_index(list, idx);
}
-
+ @DefineFunc:
+ bool consume_check(thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ if (NULL == e)
+ return false;
+ return e->written;
+ }
+ @DefineFunc:
+ call_id_t consume_id(thread_id_t tid) {
+ elem *e = get_elem_by_tid(tid);
+ if (NULL == e)
+ return DEFAULT_CALL_ID;
+ return e->id;
+ }
+ @DefineFunc:
+ void consume(thread_id_t tid) {
+ int idx = elem_idx_by_tid(tid);
+ if (idx == -1)
+ return;
+ remove_at_index(list, idx);
+ }
+ @Happens_before:
+ Prepare -> Fetch
+ Publish -> Consume
+ @End
*/
//-----------------------------------------------------
+ /**
+ @Begin
+ @Interface: Fetch
+ @Commit_point_set: Fetch_Point
+ @ID: fetch_id(__RET__)
+ @Check:
+ fetch_check(__RET__)
+ @Action:
+ fetch(__RET__);
+ @End
+ */
t_element * read_fetch() {
unsigned int rdwr = m_rdwr.load(mo_acquire);
unsigned int rd,wr;
return p;
}
+ /**
+ @Begin
+ @Interface: Consume
+ @Commit_point_set: Consume_Point
+ @ID: consume_id(__TID__)
+ @Check:
+ consume_check(__TID__)
+ @Action:
+ consume(__TID__);
+ @End
+ */
void read_consume() {
m_read.fetch_add(1,mo_release);
}
//-----------------------------------------------------
+ /**
+ @Begin
+ @Interface: Prepare
+ @Commit_point_set: Prepare_Point
+ @ID: prepare_id(__RET__)
+ @Check:
+ prepare_check(__RET__)
+ @Action:
+ prepare(__RET__);
+ @End
+ */
t_element * write_prepare() {
unsigned int rdwr = m_rdwr.load(mo_acquire);
unsigned int rd,wr;
return p;
}
+ /**
+ @Begin
+ @Interface: Publish
+ @Commit_point_set: Publish_Point
+ @ID: publish_id(__TID__)
+ @Check:
+ publish_check(__TID__)
+ @Action:
+ publish(__TID__);
+ @End
+ */
void write_publish()
{
m_written.fetch_add(1,mo_release);
public static final String HEADER_THREADS = "<threads.h>";
public static final String HEADER_STDINT = "<stdint.h>";
public static final String HEADER_MODELMEMORY = "<model_memory.h>";
- public static final String ThreadIDType = "thrd_t";
- public static final String GET_THREAD_ID = "thrd_current";
+ public static final String HEADER_MODELTYPES = "<modeltypes.h>";
+ public static final String ThreadIDType = "thread_id_t";
public static final String BOOLEAN = "bool";
public static final String UINT64 = "uint64_t";
public static final String SPEC_TAG_CURRENT = "current";
public static final String SPEC_TAG_NEXT = "next";
-
// Macro
public static final String MACRO_ID = "__ID__";
public static final String MACRO_COND = "__COND_SAT__";
public static final String MACRO_RETURN = "__RET__";
public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
+ public static final String MACRO_THREAD_ID = "__TID__";
public static void printCode(ArrayList<String> code) {
for (int i = 0; i < code.size(); i++) {
return code;
}
- private static ArrayList<String> DEFINE_ID_FUNC(String interfaceName,
- String idCode) {
+ private static ArrayList<String> DEFINE_ID_FUNC(
+ InterfaceConstruct construct, FunctionHeader header) {
+ String interfaceName = construct.name;
ArrayList<String> code = new ArrayList<String>();
- code.add("inline static " + IDType + " " + interfaceName + "_id() {");
+ String idCode = construct.idCode;
+ code.add("inline static " + IDType + " " + interfaceName + "_id("
+ + "void *info, " + ThreadIDType + " " + MACRO_THREAD_ID + ") {");
+
+ // Read info struct
+ if (!header.returnType.equals("void") || header.args.size() != 0) {
+ String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+ code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+ BRACE(infoStructType + "*") + "info"));
+ if (!header.returnType.equals("void")) {
+ code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+ GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ String type = header.args.get(i).type, var = header.args.get(i).name;
+ code.add((DECLARE_DEFINE(type, var,
+ GET_FIELD_BY_PTR(infoStructName, var))));
+ }
+ code.add("");
+ }
+
if (!idCode.equals("")) {
code.add(DECLARE_DEFINE(IDType, MACRO_ID, idCode));
} else {
String interfaceName = construct.name;
ArrayList<String> code = new ArrayList<String>();
code.add("inline static bool " + interfaceName
- + "_check_action(void *info, " + IDType + " " + MACRO_ID
- + ") {");
+ + "_check_action(void *info, " + IDType + " " + MACRO_ID + ", "
+ + ThreadIDType + " " + MACRO_THREAD_ID + ") {");
code.add(DECLARE("bool", "check_passed"));
// Read info struct
if (!header.returnType.equals("void") || header.args.size() != 0) {
headers.add(HEADER_STDLIB);
headers.add(HEADER_STDINT);
headers.add(HEADER_MODELMEMORY);
+ headers.add(HEADER_MODELTYPES);
headers.add(HEADER_SPEC_LIB);
headers.add(HEADER_STDINT);
headers.add(HEADER_CDSANNOTATE);
-// headers.add(HEADER_COMMON);
+ // headers.add(HEADER_COMMON);
headers.add(HEADER_SPECANNOTATION);
return headers;
}
ArrayList<String> newCode = new ArrayList<String>();
HashSet<String> allHeaders = getAllHeaders(semantics);
-
SequentialDefineSubConstruct code = construct.code;
// User-defined structs first
newCode.add(COMMENT("All other user-defined structs"));
// Define ID function
newCode.add(COMMENT("ID function of interface: " + interfaceName));
- newCode.addAll(DEFINE_ID_FUNC(interfaceName, iConstruct.idCode));
+ newCode.addAll(DEFINE_ID_FUNC(iConstruct, funcHeader));
newCode.add(COMMENT("End of ID function: " + interfaceName));
newCode.add("");
}
// Only generate the declaration of the wrapper, don't do any renaming
-// public static ArrayList<String> generateInterfaceWrapperDeclaration(
-// SemanticsChecker semantics, InterfaceConstruct construct) {
-// ArrayList<String> newCode = new ArrayList<String>();
-// FunctionHeader header = getFunctionHeader(semantics, construct);
-// newCode.add(COMMENT("Declaration of the wrapper"));
-// String templateStr = header.getTemplateFullStr();
-// newCode.add(templateStr);
-// newCode.add(header.getFuncStr() + ";");
-// newCode.add("");
-//
-// return newCode;
-// }
-
- public static ArrayList<String> generateInterfaceWrapperDeclaration(SemanticsChecker semantics, InterfaceConstruct construct) {
+ // public static ArrayList<String> generateInterfaceWrapperDeclaration(
+ // SemanticsChecker semantics, InterfaceConstruct construct) {
+ // ArrayList<String> newCode = new ArrayList<String>();
+ // FunctionHeader header = getFunctionHeader(semantics, construct);
+ // newCode.add(COMMENT("Declaration of the wrapper"));
+ // String templateStr = header.getTemplateFullStr();
+ // newCode.add(templateStr);
+ // newCode.add(header.getFuncStr() + ";");
+ // newCode.add("");
+ //
+ // return newCode;
+ // }
+
+ public static ArrayList<String> generateInterfaceWrapperDeclaration(
+ SemanticsChecker semantics, InterfaceConstruct construct) {
FunctionHeader header = getFunctionHeader(semantics, construct);
ArrayList<String> declaration = new ArrayList<String>();
- declaration.add(header.getRenamedHeader(SPEC_INTERFACE_WRAPPER).getDeclaration() + ";");
+ declaration.add(header.getRenamedHeader(SPEC_INTERFACE_WRAPPER)
+ .getDeclaration() + ";");
return declaration;
}
newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_INTERFACE_BEGIN,
"interface_begin"));
newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
+
String anno = "annotation_interface_begin";
newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));