case ATOMIC_TRYLOCK: {
bool success=!state->islocked;
curr->set_try_lock(success);
- if (!success)
+ if (!success) {
+ get_thread(curr)->set_return_value(0);
break;
+ }
+ get_thread(curr)->set_return_value(1);
}
//otherwise fall into the lock case
case ATOMIC_LOCK: {
+ if (curr->get_cv()->getClock(state->alloc_tid)<=state->alloc_clock) {
+ printf("Lock access before initialization\n");
+ set_assert();
+ }
state->islocked=true;
ModelAction *unlock=get_last_unlock(curr);
//synchronize with the previous unlock statement
- curr->synchronize_with(unlock);
+ if ( unlock != NULL )
+ curr->synchronize_with(unlock);
break;
}
case ATOMIC_UNLOCK: {
newcurr->copy_typeandorder(curr);
ASSERT(curr->get_location()==newcurr->get_location());
+
/* Discard duplicate ModelAction; use action from NodeStack */
delete curr;
if (!check_action_enabled(curr)) {
//we'll make the execution look like we chose to run this action
//much later...when a lock is actually available to relese
- remove_thread(get_current_thread());
get_current_thread()->set_pending(curr);
+ remove_thread(get_current_thread());
return get_next_thread(NULL);
}
build_reads_from_past(curr);
curr = newcurr;
+ /* Add the action to lists before any other model-checking tasks */
+ if (!second_part_of_rmw)
+ add_action_to_lists(newcurr);
+
+ /* Build may_read_from set for newly-created actions */
+ if (curr == newcurr && curr->is_read())
+ build_reads_from_past(curr);
+ curr = newcurr;
+
/* Thread specific actions */
switch (curr->get_type()) {
case THREAD_CREATE: {