#include <threads.h>
#include <stdlib.h>
+#include <stdatomic.h>
#include "librace.h"
#include "model-assert.h"
-#include "my_queue.h"
+
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
+
+#define MAKE_POINTER(ptr, count) ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
+
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
+
+typedef struct node {
+ unsigned int value;
+ pointer_t next;
+} node_t;
+
+typedef struct {
+ pointer_t head;
+ pointer_t tail;
+ node_t nodes[MAX_NODES + 1];
+} queue_t;
+
+void init_queue(queue_t *q, int num_threads);
+
+#include <list>
+using namespace std;
+/**
+ @Begin
+ @Global_define:
+ @DeclareStruct:
+ typedef struct tag_elem {
+ Tag id;
+ unsigned int data;
+ } tag_elem_t;
+
+ @DeclareVar:
+ list<tag_elem_t> __queue;
+ Tag tag;
+ @InitVar:
+ __queue = list<tag_elem_t>();
+ tag = 1; // Beginning of available id
+ @Happens_before:
+ # Only check the happens-before relationship according to the id of the
+ # commit_point_set. For commit_point_set that has same ID, A -> B means
+ # B happens after the previous A.
+ Enqueue -> Dequeue
+ @End
+*/
+
+
+int get_thread_num();
+
#define relaxed memory_order_relaxed
#define release memory_order_release
/* Initialize each thread's free list with INITIAL_FREE pointers */
/* The actual nodes are initialized with poison indexes */
- free_lists = malloc(num_threads * sizeof(*free_lists));
+ free_lists = (unsigned int**) malloc(num_threads * sizeof(*free_lists));
for (i = 0; i < num_threads; i++) {
for (j = 0; j < INITIAL_FREE; j++) {
free_lists[i][j] = 2 + i * MAX_FREELIST + j;
/**
@Begin
- @Interface_define: Enqueue
+ @Interface: Enqueue
+ @Commit_point_set: Enqueue_Success_Point
+ @ID: tag++
+ @Action:
+ # __ID__ is an internal macro that refers to the id of the current
+ # interface call
+ tag_elem_t elem;
+ elem.id = __ID__;
+ elem.data = val;
+ __queue.push_back(elem);
@End
*/
void enqueue(queue_t *q, unsigned int val)
&tail, value, release, release);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ == true
+ @Commit_point_define_check: commit_success == true
@Label: Enqueue_Success_Point
@End
*/
release, release);
}
-
/**
@Begin
- @Interface_define: Dequeue
+ @Interface: Dequeue
+ @Commit_point_set: Dequeue_Success_Point
+ @ID: __queue.back().id
+ @Action:
+ unsigned int _Old_Val = __queue.front().data;
+ __queue.pop_front();
+ @Post_check:
+ _Old_Val == __RET__
@End
*/
unsigned int dequeue(queue_t *q)
release, release);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ == true
+ @Commit_point_define_check: success == true
@Label: Dequeue_Success_Point
@End
*/
reclaim(get_ptr(head));
return value;
}
+
+
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+
+#include "my_queue.h"
+#include "model-assert.h"
+
+static int procs = 2;
+static queue_t *queue;
+static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
+static int num_threads;
+
+int get_thread_num()
+{
+ thrd_t curr = thrd_current();
+ int i;
+ for (i = 0; i < num_threads; i++)
+ if (curr.priv == threads[i].priv)
+ return i;
+ MODEL_ASSERT(0);
+ return -1;
+}
+
+static void main_task(void *param)
+{
+ unsigned int val;
+ int pid = *((int *)param);
+
+ if (!pid) {
+ input[0] = 17;
+ enqueue(queue, input[0]);
+ output[0] = dequeue(queue);
+ } else {
+ input[1] = 37;
+ enqueue(queue, input[1]);
+ output[1] = dequeue(queue);
+ }
+}
+
+int user_main(int argc, char **argv)
+{
+ int i;
+ int *param;
+ unsigned int in_sum = 0, out_sum = 0;
+
+ queue = (queue_t*) calloc(1, sizeof(*queue));
+ MODEL_ASSERT(queue);
+
+ num_threads = procs;
+ threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t));
+ param = (int*) malloc(num_threads * sizeof(*param));
+ input = (unsigned int*) calloc(num_threads, sizeof(*input));
+ output = (unsigned int*) calloc(num_threads, sizeof(*output));
+
+ init_queue(queue, num_threads);
+ for (i = 0; i < num_threads; i++) {
+ param[i] = i;
+ thrd_create(&threads[i], main_task, ¶m[i]);
+ }
+ for (i = 0; i < num_threads; i++)
+ thrd_join(threads[i]);
+
+ for (i = 0; i < num_threads; i++) {
+ in_sum += input[i];
+ out_sum += output[i];
+ }
+ for (i = 0; i < num_threads; i++)
+ printf("input[%d] = %u\n", i, input[i]);
+ for (i = 0; i < num_threads; i++)
+ printf("output[%d] = %u\n", i, output[i]);
+ MODEL_ASSERT(in_sum == out_sum);
+
+ free(param);
+ free(threads);
+ free(queue);
+
+ return 0;
+}
+#ifndef _MY_QUEUE_H
+#define _MY_QUEUE_H
+
#include <stdatomic.h>
#define MAX_NODES 0xf
void init_queue(queue_t *q, int num_threads);
+#include <list>
+using namespace std;
/**
@Begin
@Global_define:
typedef struct tag_elem {
Tag id;
unsigned int data;
-
- tag_elem(Tag _id, unsigned int _data) {
- id = _id;
- data = _data;
- }
} tag_elem_t;
+
@DeclareVar:
- spec_queue<tag_elem_t> queue;
+ list<tag_elem_t> __queue;
Tag tag;
@InitVar:
- queue = spec_queue<tag_elem_t>();
- tag = Tag();
+ __queue = list<tag_elem_t>();
+ tag = 1; // Beginning of available id
@Happens_before:
# Only check the happens-before relationship according to the id of the
# commit_point_set. For commit_point_set that has same ID, A -> B means
@Begin
@Interface: Enqueue
@Commit_point_set: Enqueue_Success_Point
- @ID: __sequential.tag.getCurAndInc()
+ @ID: tag++
@Action:
# __ID__ is an internal macro that refers to the id of the current
# interface call
- __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+ tag_elem_t elem;
+ elem.id = __ID__;
+ elem.data = val;
+ __queue.push_back(elem);
@End
*/
void enqueue(queue_t *q, unsigned int val);
@Begin
@Interface: Dequeue
@Commit_point_set: Dequeue_Success_Point
- @ID: __sequential.queue.peak().tag
+ @ID: __queue.back().id
@Action:
- unsigned int _Old_Val = __sequential.queue.dequeue().data;
+ unsigned int _Old_Val = __queue.front().data;
+ __queue.pop_front();
@Post_check:
_Old_Val == __RET__
@End
*/
unsigned int dequeue(queue_t *q);
int get_thread_num();
+
+#endif
<COLON: ":">
|
<DOUBLECOLON: "::">
+|
+ <DOUBLELESSTHAN: "<<">
+|
+ <DOUBLEGREATERTHAN: ">>">
+|
+ <TRIPLEGREATERTHAN: ">>>">
+|
+ <PLUS_EQUALS: "+=">
+|
+ <MINUS_EQUALS: "-=">
+|
+ <TIMES_EQUALS: "*=">
+|
+ <DIVIDE_EQUALS: "/=">
+|
+ <MOD_EQUALS: "%=">
+|
+ <XOR_EQUALS: "^=">
+|
+ <OR_EQUALS: "|=">
+|
+ <AND_EQUALS: "&=">
+
|
<SEMI_COLON: ";">
|
t = <GREATER_EQUALS> | t = <LESS_EQUALS> |
t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
+ t = <DOUBLELESSTHAN> |
+ t = <DOUBLEGREATERTHAN> |
+ t = <TRIPLEGREATERTHAN> |
+
+ t = <PLUS_EQUALS> |
+ t = <MINUS_EQUALS> |
+ t = <TIMES_EQUALS> |
+ t = <DIVIDE_EQUALS> |
+ t = <MOD_EQUALS> |
+ t = <XOR_EQUALS> |
+ t = <OR_EQUALS> |
+ t = <AND_EQUALS> |
+
(t = <SEMI_COLON> { newLine = true; } )
| t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL> |
public static void main(String[] argvs) {
String homeDir = Environment.HOME_DIRECTORY;
File[] srcFiles = {
- new File(Environment.MODEL_CHECKER_TEST_DIR + "/backup_linuxrwlocks.c") };
-// new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+// new File(Environment.MODEL_CHECKER_TEST_DIR + "/backup_linuxrwlocks.c") };
+ new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
// new File(homeDir
// + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
- // new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
- // new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+// new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+// new File(homeDir + "/benchmark/ms-queue/my_queue.c") };
// new File(homeDir + "/benchmark/test/test.c") };
CodeGenerator gen = new CodeGenerator(srcFiles);
gen.generateCode();
newCode.add("}");
newCode.add("");
}
+ // Also add the true condition if any
+ if (semantics.containsConditionalInterface(new ConditionalInterface(interfaceName, ""))) {
+ structName = "hb_condition";
+ newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_CONDITION, structName));
+ newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
+ newCode.add(ASSIGN_TO_PTR(structName, "hb_condition_num", "0"));
+ anno = "annotation_hb_condition";
+ newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
+ newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
+ newCode.add(ANNOTATE(anno));
+ newCode.add("");
+ }
// Interface end
String infoStructType = null, infoName = null;
if (!header.returnType.equals("void") || header.args.size() > 0) {
newCode.add(COMMENT("Include redundant headers"));
newCode.add(INCLUDE(HEADER_STDINT));
newCode.add(INCLUDE(HEADER_CDSANNOTATE));
+ newCode.add(INCLUDE(HEADER_SPECANNOTATION));
newCode.add("");
// Add annotation
newCode.add("if (" + construct.condition + ") {");
public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
return this.hbConditions;
}
+
+ /**
+ * Check if the conditional interface is in the HB checking list
+ * @param condInterface
+ * @return
+ */
+ public boolean containsConditionalInterface(ConditionalInterface condInterface) {
+ if (hbConditions.containsKey(condInterface))
+ return true;
+ for (ConditionalInterface key : hbConditions.keySet()) {
+ if (hbConditions.get(key).contains(condInterface))
+ return true;
+ }
+ return false;
+ }
public String getOption(String key) {
return options.get(key);
public class ConditionalInterface {
public final String interfaceName;
public final String hbConditionLabel;
-
+
public ConditionalInterface(String interfaceName, String hbConditionLabel) {
this.interfaceName = interfaceName;
this.hbConditionLabel = hbConditionLabel;
}
-
- public boolean equals(ConditionalInterface other) {
+
+ public boolean equals(Object other) {
if (!(other instanceof ConditionalInterface))
return false;
ConditionalInterface another = (ConditionalInterface) other;
- return another.interfaceName.equals(interfaceName) &&
- another.hbConditionLabel.equals(hbConditionLabel);
+ return another.interfaceName.equals(interfaceName)
+ && (another.hbConditionLabel.equals(hbConditionLabel) || another.hbConditionLabel
+ .equals(""));
}
-
+
public int hashCode() {
return interfaceName.hashCode() << 5 ^ hbConditionLabel.hashCode();
}
-
+
public String toString() {
if (hbConditionLabel.equals(""))
return interfaceName + "(true)";
projects / cdsspec-compiler.git / commitdiff