bdemsky / cdschecker

CDSChecker Model Checker for C++11 Atomics
GNU General Public License v2.0
0 stars 1 forks source link

Assertion tripped by atomics test code #1

Open melintea opened 1 week ago

melintea commented 1 week ago

This test code trips the assertion at execution.cc line 1087 Played around with other atomics tests and it the assertion is regularily trigerred.

I do not think it is relevant: Ubuntu, using g++12 and/or clang18


// https://github.com/melintea/CDSChecker/blob/main/test/relacy-good.cc
//
// Same test as the relacy one
//

#include "common.h"
#include "librace.h"

#include <atomic>
#include <threads.h>
#include <stdio.h>
#include <unistd.h>

std::atomic<int> a{0};
int x = 0; // dependent data

void fa(void *obj)
{
    x = 1;
    // bug: use rl::mo_relaxed aka std::memory_order_relaxed
    // fix: use rl::mo_release aka std::memory_order_release
    a.store(1, std::memory_order_release);
}

void fb(void *obj)
{
    // bug: use rl::mo_relaxed aka std::memory_order_relaxed
    // fix: use rl::mo_acquire aka std::memory_order_acquire
    if (1 == a.load(std::memory_order_acquire))
    {
        x = 2;
    }
}

int user_main(int argc, char **argv)
{
    //sleep(15);
    a.store(0, std::memory_order_release);

    thrd_t t1, t2;

    printf("Main thread: creating 2 threads\n");
    thrd_create(&t1, (thrd_start_t)&fa, NULL);
    thrd_create(&t2, (thrd_start_t)&fb, NULL);

    thrd_join(t1);
    thrd_join(t2);
    printf("Main thread is finished\n");

    return 0;
}
bdemsky commented 1 week ago

I tried your test case from the CDSChecker version on GitHub on Ubuntu Linux. After adding --std=c++11, CDSChecker compiled. Then your test case seemed to run without any issue for me using run.sh. CDSChecker isn't really actively maintained these days by us.

melintea commented 1 week ago

Thank you for looking into. I forgot to mention - my apologies: I am using the master branch,

This change does not trigger the assert. I think it is a safe change but I am really new to the codebase.

$ git diff
diff --git a/execution.cc b/execution.cc
index b90c52f..0c80648 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1084,8 +1084,10 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                if ((*curr)->is_rmwr())
                        newcurr->copy_typeandorder(*curr);

-               ASSERT((*curr)->get_location() == newcurr->get_location());
+               ASSERT(  ((*curr)->get_location() == newcurr->get_location())
+                     || ((*curr)->get_type() == THREAD_START && newcurr->get_type() == THREAD_START)
+                     || ((*curr)->get_type() == THREAD_FINISH && newcurr->get_type() == THREAD_FINISH)
+                     );
                newcurr->copy_from_new(*curr);

                /* Discard duplicate ModelAction; use action from NodeStack */