#include <threads.h>
#include <stdatomic.h>
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
#include "librace.h"
#define RW_LOCK_BIAS 0x00100000
/**
@Begin
+ @Options:
+ LANG = C;
@Global_define:
@DeclareVar:
bool writer_lock_acquired;
@Happens_before:
# Since commit_point_set has no ID attached, A -> B means that for any B,
# the previous A happens before B.
+ #Read_Unlock -> Read_Lock
+ Read_Unlock -> Write_Lock
+ Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+ #Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
Write_Unlock -> Write_Lock
Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
Write_Unlock -> Read_Lock
Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
+ @Commutativity: Read_Lock <-> Read_Lock: true
+ @Commutativity: Read_Lock <-> Read_Unlock: true
+ @Commutativity: Read_Lock <-> Read_Trylock: true
+ @Commutativity: Read_Lock <-> Write_Trylock: !_Method2.__RET__
+
+ @Commutativity: Read_Unlock <-> Read_Unlock: true
+ @Commutativity: Read_Unlock <-> Read_Trylock: true
+ @Commutativity: Read_Unlock <-> Write_Trylock: !_Method2.__RET__
+
+ @Commutativity: Read_Trylock <-> Read_Trylock: true
+ @Commutativity: Read_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+ @Commutativity: Read_Trylock <-> Write_Lock: !_Method1.__RET__
+ @Commutativity: Read_Trylock <-> Write_Unlock: !_Method1.__RET__
+
+ @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
+ @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
+ @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
@End
*/
/**
@Begin
@Interface: Read_Lock
- @Commit_point_set:
- Read_Lock_Success_1 | Read_Lock_Success_2
- @Check:
- !writer_lock_acquired
- @Action:
- reader_lock_cnt++;
+ @Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
+ @Check: !writer_lock_acquired
+ @Action: reader_lock_cnt++;
@End
*/
static inline void read_lock(rwlock_t *rw)
{
+
+ /********** Admissibility **********/
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
thrd_yield();
}
+ /********** Admissibility **********/
priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
/**
@Begin
@Interface: Write_Lock
- @Commit_point_set:
- Write_Lock_Success_1 | Write_Lock_Success_2
- @Check:
- !writer_lock_acquired && reader_lock_cnt == 0
- @Action:
- writer_lock_acquired = true;
+ @Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
+ @Check: !writer_lock_acquired && reader_lock_cnt == 0
+ @Action: writer_lock_acquired = true;
@End
*/
static inline void write_lock(rwlock_t *rw)
{
+ /********** Admissibility **********/
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
thrd_yield();
}
+ /********** Admissibility **********/
priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
/**
@Begin
@Interface: Read_Trylock
- @Commit_point_set:
- Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
- @Condition:
- writer_lock_acquired == false
- @HB_condition:
- HB_Read_Trylock_Succ :: __RET__ == 1
+ @Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
+ //@Condition: writer_lock_acquired == false
+ @HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
@Action:
- if (__COND_SAT__)
+ if (__RET__)
reader_lock_cnt++;
- @Post_check:
- __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+ @Post_check: __RET__ == !writer_lock_acquired || !__RET__
@End
*/
static inline int read_trylock(rwlock_t *rw)
{
+ /********** Admissibility **********/
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
- @Potential_commit_point: true
+ @Potential_commit_point_define: true
@Label: Potential_Read_Trylock_Point
@End
*/
/**
@Begin
@Commit_point_define: true
- @Label: Read_Trylock_Succ_Point
@Potential_commit_point_label: Potential_Read_Trylock_Point
+ @Label: Read_Trylock_Succ_Point
@End
*/
return 1;
/**
@Begin
@Commit_point_define: true
- @Label: Read_Trylock_Fail_Point
@Potential_commit_point_label: Potential_Read_Trylock_Point
+ @Label: Read_Trylock_Fail_Point
@End
*/
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
/**
@Begin
@Interface: Write_Trylock
- @Commit_point_set:
- Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
- @Condition:
- !writer_lock_acquired && reader_lock_cnt == 0
- @HB_condition:
- HB_Write_Trylock_Succ :: __RET__ == 1
+ @Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
+ @HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
@Action:
- if (__COND_SAT__)
+ if (__RET__ == 1)
writer_lock_acquired = true;
- @Post_check:
- __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
@End
*/
static inline int write_trylock(rwlock_t *rw)
{
+ /********** Admissibility **********/
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+ //model_print("write_trylock: priorvalue: %d\n", priorvalue);
/**
@Begin
- @Potential_commit_point: true
+ @Potential_commit_point_define: true
@Label: Potential_Write_Trylock_Point
@End
*/
/**
@Begin
@Commit_point_define: true
- @Label: Write_Trylock_Succ_Point
@Potential_commit_point_label: Potential_Write_Trylock_Point
+ @Label: Write_Trylock_Succ_Point
@End
*/
return 1;
/**
@Begin
@Commit_point_define: true
- @Label: Write_Trylock_Fail_Point
@Potential_commit_point_label: Potential_Write_Trylock_Point
+ @Label: Write_Trylock_Fail_Point
@End
*/
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
@Begin
@Interface: Read_Unlock
@Commit_point_set: Read_Unlock_Point
- @Check:
- reader_lock_cnt > 0 && !writer_lock_acquired
- @Action:
- reader_lock_cnt--;
+ @Check: reader_lock_cnt > 0 && !writer_lock_acquired
+ @Action: reader_lock_cnt--;
@End
*/
static inline void read_unlock(rwlock_t *rw)
{
+ /********** Admissibility **********/
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
/**
@Begin
/**
@Begin
@Interface: Write_Unlock
- @Commit_point_set: Write_Unlock_Point
- @Check:
- reader_lock_cnt == 0 && writer_lock_acquired
- @Action:
- writer_lock_acquired = false;
+ @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
+ @Check: reader_lock_cnt == 0 && writer_lock_acquired
+ @Action: writer_lock_acquired = false;
@End
*/
static inline void write_unlock(rwlock_t *rw)
{
+ /********** Admissibility **********/
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
/**
@Begin
@Label: Write_Unlock_Point
@End
*/
+
+ /**
+ //@Begin
+ @Commit_point_clear: true
+ @Label: Write_Unlock_Clear
+ @End
+ */
}
rwlock_t mylock;
static void a(void *obj)
{
- int i;
- for(i = 0; i < 2; i++) {
- if ((i % 2) == 0) {
- read_lock(&mylock);
- load_32(&shareddata);
- read_unlock(&mylock);
- } else {
- write_lock(&mylock);
- store_32(&shareddata,(unsigned int)i);
- write_unlock(&mylock);
- }
+ read_lock(&mylock);
+ //load_32(&shareddata);
+ //printf("%d\n", shareddata);
+ read_unlock(&mylock);
+
+ write_lock(&mylock);
+ //store_32(&shareddata,(unsigned int)i);
+ shareddata = 47;
+ write_unlock(&mylock);
+}
+
+static void b(void *obj)
+{
+ if (read_trylock(&mylock) == 1) {
+ //printf("%d\n", shareddata);
+ read_unlock(&mylock);
+ }
+
+ if (write_trylock(&mylock) == 1) {
+ //shareddata = 47;
+ write_unlock(&mylock);
}
}
atomic_init(&mylock.lock, RW_LOCK_BIAS);
thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&a, NULL);
+ thrd_create(&t2, (thrd_start_t)&b, NULL);
thrd_join(t1);
thrd_join(t2);
projects / cdsspec-compiler.git / blobdiff