projects
/
cdsspec-compiler.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
changes with lines of spec counted
[cdsspec-compiler.git]
/
benchmark
/
mpmc-queue
/
mpmc-queue.h
diff --git
a/benchmark/mpmc-queue/mpmc-queue.h
b/benchmark/mpmc-queue/mpmc-queue.h
index d482c9e9790b62d430637b1ec9c222a386199b4a..aa1012976ee8501596d27cc7852f9006ea0e1e0c 100644
(file)
--- a/
benchmark/mpmc-queue/mpmc-queue.h
+++ b/
benchmark/mpmc-queue/mpmc-queue.h
@@
-48,20
+48,23
@@
public:
LANG = CPP;
CLASS = mpmc_boundq_1_alt;
@Global_define:
LANG = CPP;
CLASS = mpmc_boundq_1_alt;
@Global_define:
- @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;
+
//
@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;
//id_tag_t *tag;
-
@InitVar:
-
list = new_spec_list();
+
//
@InitVar:
+
//
list = new_spec_list();
//tag = new_id_tag();
//tag = new_id_tag();
+ // @Cleanup:
+// if (list)
+// free_spec_list();
@Happens_before:
Publish -> Fetch
Consume -> Prepare
@Happens_before:
Publish -> Fetch
Consume -> Prepare
@@
-73,7
+76,7
@@
public:
/**
@Begin
@Interface: Fetch
/**
@Begin
@Interface: Fetch
- @Commit_point_set: Fetch_
Empty_Point | Fetch_Succ_Point
+ @Commit_point_set: Fetch_
RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
@ID: (call_id_t) __RET__
//@Check:
//__RET__ == NULL || has_elem(list, __RET__)
@ID: (call_id_t) __RET__
//@Check:
//__RET__ == NULL || has_elem(list, __RET__)
@@
-81,12
+84,12
@@
public:
*/
t_element * read_fetch() {
// Try this new weaker semantics
*/
t_element * read_fetch() {
// Try this new weaker semantics
-
//
unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_relaxed);
+ unsigned int rdwr = m_rdwr.load(mo_acquire);
+
//
unsigned int rdwr = m_rdwr.load(mo_relaxed);
/**
@Begin
@Potential_commit_point_define: true
/**
@Begin
@Potential_commit_point_define: true
- @Label: Fetch_Potential_
Point
+ @Label: Fetch_Potential_
RW_Load
@End
*/
unsigned int rd,wr;
@End
*/
unsigned int rd,wr;
@@
-99,8
+102,8
@@
public:
/**
@Begin
@Commit_point_define: true
/**
@Begin
@Commit_point_define: true
- @Potential_commit_point_label: Fetch_Potential_
Point
- @Label: Fetch_
Empty_Point
+ @Potential_commit_point_label: Fetch_Potential_
RW_Load
+ @Label: Fetch_
RW_Load_Empty
@End
*/
@End
*/
@@
-110,8
+113,8
@@
public:
bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
/**
@Begin
bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
/**
@Begin
- @Commit_point_define_check: succ
== true
- @Label: Fetch_
Succ_Point
+ @Commit_point_define_check: succ
+ @Label: Fetch_
RW_RMW
@End
*/
if (succ)
@End
*/
if (succ)
@@
-122,9
+125,28
@@
public:
// (*1)
rl::backoff bo;
// (*1)
rl::backoff bo;
- while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
- thrd_yield();
+ while (true) {
+ int written = m_written.load(mo_acquire);
+ /**
+ @Begin
+ @Potential_commit_point_define: true
+ @Label: Fetch_Potential_W_Load
+ @End
+ */
+ if ((written & 0xFFFF) != wr) {
+ thrd_yield();
+ } else {
+ break;
+ }
}
}
+
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Fetch_Potential_W_Load
+ @Label: Fetch_W_Load
+ @End
+ */
t_element * p = & ( m_array[ rd % t_size ] );
t_element * p = & ( m_array[ rd % t_size ] );
@@
-134,7
+156,7
@@
public:
/**
@Begin
@Interface: Consume
/**
@Begin
@Interface: Consume
- @Commit_point_set: Consume_
Point
+ @Commit_point_set: Consume_
R_RMW
@ID: (call_id_t) bin
//@Check:
// consume_check(__TID__)
@ID: (call_id_t) bin
//@Check:
// consume_check(__TID__)
@@
-143,11
+165,12
@@
public:
@End
*/
void read_consume(t_element *bin) {
@End
*/
void read_consume(t_element *bin) {
+ /**** FIXME: miss ****/
m_read.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
m_read.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
- @Label: Consume_
Point
+ @Label: Consume_
R_RMW
@End
*/
}
@End
*/
}
@@
-157,7
+180,7
@@
public:
/**
@Begin
@Interface: Prepare
/**
@Begin
@Interface: Prepare
- @Commit_point_set: Prepare_
Full_Point | Prepare_Succ_Point
+ @Commit_point_set: Prepare_
RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
@ID: (call_id_t) __RET__
//@Check:
//prepare_check(__RET__, __TID__)
@ID: (call_id_t) __RET__
//@Check:
//prepare_check(__RET__, __TID__)
@@
-167,12
+190,12
@@
public:
*/
t_element * write_prepare() {
// Try weaker semantics
*/
t_element * write_prepare() {
// Try weaker semantics
-
//
unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_relaxed);
+ unsigned int rdwr = m_rdwr.load(mo_acquire);
+
//
unsigned int rdwr = m_rdwr.load(mo_relaxed);
/**
@Begin
@Potential_commit_point_define: true
/**
@Begin
@Potential_commit_point_define: true
- @Label: Prepare_Potential_
Point
+ @Label: Prepare_Potential_
RW_Load
@End
*/
unsigned int rd,wr;
@End
*/
unsigned int rd,wr;
@@
-185,8
+208,8
@@
public:
/**
@Begin
@Commit_point_define: true
/**
@Begin
@Commit_point_define: true
- @Potential_commit_point_label: Prepare_Potential_
Point
- @Label: Prepare_
Full_Point
+ @Potential_commit_point_label: Prepare_Potential_
RW_Load
+ @Label: Prepare_
RW_Load_Full
@End
*/
return NULL;
@End
*/
return NULL;
@@
-196,8
+219,8
@@
public:
((wr+1)&0xFFFF),mo_acq_rel);
/**
@Begin
((wr+1)&0xFFFF),mo_acq_rel);
/**
@Begin
- @Commit_point_define_check: succ
== true
- @Label: Prepare_
Succ_Point
+ @Commit_point_define_check: succ
+ @Label: Prepare_
RW_RMW
@End
*/
if (succ)
@End
*/
if (succ)
@@
-208,10
+231,28
@@
public:
// (*1)
rl::backoff bo;
// (*1)
rl::backoff bo;
- while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
- thrd_yield();
+ while (true) {
+ int read = m_read.load(mo_acquire);
+ /**
+ @Begin
+ @Potential_commit_point_define: true
+ @Label: Prepare_Potential_R_Load
+ @End
+ */
+ if ((read & 0xFFFF) != rd)
+ thrd_yield();
+ else
+ break;
}
}
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Prepare_Potential_R_Load
+ @Label: Prepare_R_Load
+ @End
+ */
+
t_element * p = & ( m_array[ wr % t_size ] );
return p;
t_element * p = & ( m_array[ wr % t_size ] );
return p;
@@
-220,7
+261,7
@@
public:
/**
@Begin
@Interface: Publish
/**
@Begin
@Interface: Publish
- @Commit_point_set: Publish_
Point
+ @Commit_point_set: Publish_
W_RMW
@ID: (call_id_t) bin
//@Check:
//publish_check(__TID__)
@ID: (call_id_t) bin
//@Check:
//publish_check(__TID__)
@@
-230,11
+271,12
@@
public:
*/
void write_publish(t_element *bin)
{
*/
void write_publish(t_element *bin)
{
+ /**** hb violation ****/
m_written.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
m_written.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
- @Label: Publish_
Point
+ @Label: Publish_
W_RMW
@End
*/
}
@End
*/
}