Question about "A Simple Threads Example (threads.c)"

[AiDaiP]

When I run the example in MANUAL

    int shared = 0;
    int *ptr;

    void
    thread1(void)
    {       int tmp;
            ptr = &shared;
            tmp = shared;
            tmp++;
            shared = tmp;
    }

    void
    thread2(void)
    {       int tmp;
            if (ptr)
            {       tmp = shared;
                    tmp++;
                    shared = tmp;
                    assert(shared == 1);
            }
    }

The result is:

verify threads.c

        Extract Model:
        ==============
modex threads.c
MODEX Version 2.11 - 3 November 2017
created: model and _modex_.run

        Compile and Run:
        ================
sh _modex_.run

(Spin Version 6.5.1 -- 3 June 2021)
        + Partial Order Reduction

Hash-Compact 4 search for:
        never claim             - (none specified)
        assertion violations    +
        acceptance   cycles     - (not selected)
        invalid end states      +

State-vector 96 byte, depth reached 0, errors: 0
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000       equivalent memory usage for states (stored*(State-vector + overhead))
    0.290       actual memory usage for states
 4096.000       memory used for hash table (-w29)
    0.534       memory used for DFS stack (-m10000)
 4096.730       total actual memory usage

pan: elapsed time 0 seconds

No Errors Found

Why it doesn't find the error like the example?

[nimble-code]

I just reran that example on my system -- same version of modex and same version of spin -- and I get the result shown in the MANUAL -- so something is different on your system. perhaps check that the model generated is correct? it should be in the file "model" after you run "verify" and should look like this: 1 // Generated by MODEX Version 2.11 - 3 November 2017 2 // Thu, Dec 30, 2021 9:48:51 AM from threads.c 3 4 c_state "int * ptr" "Global" 5 int shared = 0; 6 active proctype p_thread1( ) 7 { 8 int tmp; 9 c_code { now.ptr=(&(now.shared)); }; 10 c_code { Pp_thread1->tmp=now.shared; }; 11 c_code { Pp_thread1->tmp++; }; 12 c_code { now.shared=Pp_thread1->tmp; }; 13 } 14 active proctype p_thread2( ) 15 { 16 int tmp; 17 if 18 :: c_expr { now.ptr }; 19 c_code { Pp_thread2->tmp=now.shared; }; 20 c_code { Pp_thread2->tmp++; }; 21 c_code { now.shared=Pp_thread2->tmp; }; 22 c_code [(now.shared==1)] { ; }; 23 :: c_expr { !now.ptr }; 24 fi; 25 }

[AiDaiP]

This is my system info:

Linux aidai-virtual-machine 5.11.0-43-generic #47~20.04.2-Ubuntu SMP Mon Dec 13 11:06:56 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux
AMD EPYC 7742 64-Core @ 16x 2.25GHz
gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04)

The model is:

// Generated by MODEX Version 2.11 - 3 November 2017
// 2021年 12月 31日 星期五 09:12:51 CST from threads.c

bool lck_p_thread2_ret;
bool lck_p_thread2;
bool lck_p_thread1_ret;
bool lck_p_thread1;
 c_state "int  * ptr" "Global"
int shared = 0;
chan ret_p_thread2 = [1] of { pid };
chan exc_cll_p_thread2 = [0] of { pid };
chan req_cll_p_thread2 = [1] of { pid };
chan ret_p_thread1 = [1] of { pid };
chan exc_cll_p_thread1 = [0] of { pid };
chan req_cll_p_thread1 = [1] of { pid };
active proctype p_thread1( )
{
int tmp;
pid lck_id;
endRestart:
 atomic {
 nempty(req_cll_p_thread1) && !lck_p_thread1 -> lck_p_thread1 = 1;
 req_cll_p_thread1?lck_id; exc_cll_p_thread1?eval(lck_id);
 lck_p_thread1 = 0;
 };
    c_code { now.ptr=(&(now.shared)); };
    c_code { Pp_thread1->tmp=now.shared; };
c_code { Pp_thread1->tmp++; };
    c_code { now.shared=Pp_thread1->tmp; };
Return: skip;
 ret_p_thread1!lck_id;
 goto endRestart
}
active proctype p_thread2( )
{
int tmp;
pid lck_id;
endRestart:
 atomic {
 nempty(req_cll_p_thread2) && !lck_p_thread2 -> lck_p_thread2 = 1;
 req_cll_p_thread2?lck_id; exc_cll_p_thread2?eval(lck_id);
 lck_p_thread2 = 0;
 };
    if
    :: c_expr { now.ptr };
        c_code { Pp_thread2->tmp=now.shared; };
c_code { Pp_thread2->tmp++; };
        c_code { now.shared=Pp_thread2->tmp; };
        c_code [(now.shared==1)] { ; };
    :: c_expr { !now.ptr };
 fi;
Return: skip;
 ret_p_thread2!lck_id;
 goto endRestart
}

[nimble-code]

very odd -- did you modify threads.c or threads.prx in any way?

[AiDaiP]

I just copy it from the MANUAL.