need more examples

[hazardpl]

dear author, 1、would you please gvie me some more complex examples such as multi-threading exaxmple using and 。 2、and I do need some ebook about modex for beginner ,like me : )

thanks!

[hazardpl]

1、such as multi-threading exaxmple using thread and pthread,

[nimble-code]

this chapter explains the use of embedded C code, that the model extractor makes use of, in some detail: http://spinroot.com/spin/Doc/spin4_ch17.pdf there's also the online course that covers model extraction, and there are the examples within this distribution: https://github.com/nimble-code/Modex/tree/master/Examples You're saying that this isn't sufficient? If so, let me know which issues you're unsure about?

[nimble-code]

the online course is: http://spinroot.com/course/

[hazardpl]

include<sys/types.h>

include

include

include

include

include

include

define NUM 3

pthread_cond_t condv = PTHREAD_COND_INITIALIZER; pthread_mutex_t mlock = PTHREAD_MUTEX_INITIALIZER;

void producer(void* arg) { int n = NUM; while(n--) { sleep(1); pthread_cond_signal(&condv); printf("producer thread send notify signal. %d\t", NUM-n); } }

void consumer(void* arg) { int n = 0; while (1) { pthread_cond_wait(&condv, &mlock); printf("recv producer thread notify signal. %d\n", ++n); if (NUM == n) { break; } } }

int main() { pthread_t tid1, tid2; pthread_create(&tid1, NULL, (void)producer, NULL); pthread_create(&tid2, NULL, (void)consumer, NULL);

pthread_join(tid1, NULL);
pthread_join(tid2, NULL);

return 0;

}

//when I use command modex test.c command and spin -a the .pml file
//spin will report : //C:\Modex-master\test_modex>spin -a modex.pml //spin: modex.h:15, Error: undeclared variable: PTHREAD_MUTEX_INITIALIZER statement separator near 'int'

[hazardpl]

include

include

include

define NUM_Threads 5

void PrintHelloId(void threadid) { int tid = ((int )threadid); printf("Hello,World， Thread %d\n",tid); return 0; }

int main() { pthread_t pthreads[NUM_Threads]; int i, rc; int indexes[NUM_Threads];

for (i=0; i<NUM_Threads; i++)
{
    printf("main() : create thread %d \n",i);
    indexes[i] = i; 
    rc = pthread_create(&pthreads[i], NULL, PrintHelloId, (void *)&indexes[i]);
    if (0 != rc)
    {
        printf("Error\n");
        exit(-1);
    }
}

pthread_exit(NULL);
return 0;

}

//C:\Modex-master\test_modex>modex test_a.c //MODEX Version 2.11 - 3 November 2017 //modex: error: local tid is initialized in declaration in instrumented PrintHell //oId() //could you tell me why modex report this error, thank you!

[hazardpl]

//if I use Non-Posix C thread ,such as C++11 thread

include

include

include // std::cout

include // std::thread

void thread_task() { std::cout << "hello thread" << std::endl; } int main(int argc, const char *argv[]) { std::thread t(thread_task); t.join(); return EXIT_SUCCESS; }

//for the code above, the modex will report error ,so //if my program is written by Non-Posix C thread ,do I have an easy way to verify the code?

[hazardpl]

I a beginner for modex and spin . So I really hope you can give me a more detailed answer. Thank you very much. I am using cygwin and minGW environment to run modex and spin tools. my OS is window7

[nimble-code]

i'll look into it, to see if i can reproduce what you're reporting

[nimble-code]

Modes can process only ISO/ANSI C code, not C++ code, so the example you showed can't be handled alas.

On Mon, Jul 20, 2020 at 1:48 AM hazardpl notifications@github.com wrote:

//if I use Non-Posix C thread ,such as C++11 thread

include

include

include // std::cout

include // std::thread

void thread_task() { std::cout << "hello thread" << std::endl; } int main(int argc, const char *argv[]) { std::thread t(thread_task); t.join(); return EXIT_SUCCESS; }

//for the code above, the modex will report error ,so //if my program is written by Non-Posix C thread ,do I have an easy way to verify the code?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/nimble-code/Modex/issues/2#issuecomment-660893746, or unsubscribe https://github.com/notifications/unsubscribe-auth/AK6L6INXXJ5KYLTM5YNLDA3R4QAGDANCNFSM4O2HDPBQ .

[nimble-code]

the include files aren't processed by Modex, so you'll need to provide definitions for symbols that otherwise cannot be recognized. the easiest way to do so would be to use a -D argument on the command line, e.g. by saying -DPTHREAD_MUTEX_INITIALIZER=0 (this is just to help the parser absorb the code, so any value can do here. the same principle can be used for defining unrecognized types, by mapping them to "int" with a -D argument. you can separately look if you need to address related issues in the generated model, using a lookup table for instance.

On Mon, Jul 20, 2020 at 1:16 AM hazardpl notifications@github.com wrote:

include<sys/types.h>

include

include

include

include

include

include

define NUM 3

pthread_cond_t condv = PTHREAD_COND_INITIALIZER; pthread_mutex_t mlock = PTHREAD_MUTEX_INITIALIZER;

void producer(void* arg) { int n = NUM; while(n--) { sleep(1); pthread_cond_signal(&condv); printf("producer thread send notify signal. %d\t", NUM-n); } }

void consumer(void* arg) { int n = 0; while (1) { pthread_cond_wait(&condv, &mlock); printf("recv producer thread notify signal. %d\n", ++n); if (NUM == n) { break; } } }

int main() { pthread_t tid1, tid2; pthread_create(&tid1, NULL, (void)producer, NULL); pthread_create(&tid2, NULL, (void)consumer, NULL);

pthread_join(tid1, NULL); pthread_join(tid2, NULL);

return 0;

}

//when I use command modex test.c command and spin -a the .pml file //spin will report : //C:\Modex-master\test_modex>spin -a modex.pml //spin: modex.h:15, Error: undeclared variable: PTHREAD_MUTEX_INITIALIZER statement separator near 'int'

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/nimble-code/Modex/issues/2#issuecomment-660877226, or unsubscribe https://github.com/notifications/unsubscribe-auth/AK6L6IOXVZJN4H3S5LRTTVTR4P4N3ANCNFSM4O2HDPBQ .

[nimble-code]

the documentation for modex explains that the parser has trouble with initialized data in declarations. separating the initialization from the declaration can help avoid this. (note that modex isn't a tool for new spin users -- even for advanced users it can be challenging)

On Mon, Jul 20, 2020 at 1:42 AM hazardpl notifications@github.com wrote:

include

include

include

define NUM_Threads 5

void PrintHelloId(void threadid) { int tid = ((int )threadid); printf("Hello,World， Thread %d\n",tid); return 0; }

int main() { pthread_t pthreads[NUM_Threads]; int i, rc; int indexes[NUM_Threads];

for (i=0; i<NUM_Threads; i++)

{

printf("main() : create thread %d \n",i);

indexes[i] = i;

rc = pthread_create(&pthreads[i], NULL, PrintHelloId, (void *)&indexes[i]);

if (0 != rc)

{

    printf("Error\n");

    exit(-1);

}

}

pthread_exit(NULL);

return 0;

}

//C:\Modex-master\test_modex>modex test_a.c //MODEX Version 2.11 - 3 November 2017 //modex: error: local tid is initialized in declaration in instrumented PrintHell //oId() //could you tell me why modex report this error, thank you!

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/nimble-code/Modex/issues/2#issuecomment-660890554, or unsubscribe https://github.com/notifications/unsubscribe-auth/AK6L6IKHTJ4FRE4ME4XEEJLR4P7OBANCNFSM4O2HDPBQ .

[hazardpl]

Thank you for such a detailed answer, looking forward to discussing with you in the future. : )

[zhang-cell]

Dear author： Do you know why the sixth case GCC - O pan pan. C in the modex example will produce an error after compiling zkwdl@ubuntu :~/urs/local/bun/Modex-master/Examples$ modex 6 suspend.prx MODEX Version 2.11 - 3 November 2017 created: model and modex .run zkwdl@ubuntu :~/urs/local/bun/Modex-master/Examples$ spin -a model zkwdl@ubuntu :~/urs/local/bun/Modex-master/Examples$ gcc -o -pan pan.c In file included from pan.c:5876:0: pan.m: In function ‘do transit’: pan.m:28:14: warning: implicit declaration of function ‘mutex lock’; did you mean ‘spin mutex lock’? [-Wimplicit-function-declaration] sv save(); mutex lock((&( now.count lock))); } ^~~~~~ spin mutex lock pan.m:64:14: warning: implicit declaration of function ‘mutex unlock’; did you mean ‘spin mutex unlock’? [-Wimplicit-function-declaration] sv save(); mutex unlock((&( now.count lock))); } ^~~~ spin mutex unlock /tmp/cc1bErd8.o: In function do_ transit': pan.c:(.text+0x2e96): undefined reference tomutex lock' pan.c:(.text+0x2f18): undefined reference to `mutex unlock' pan.c:(.text+0x2fe8): undefined reference to mutex_ lock' pan.c:(.text+0x3015): undefined reference tomutex_ unlock' collect2: error: ld returned 1 exit status

[nimble-code]

The source code for Modex does not contain any use of mutex_lock, only spin_mutex_lock. But, the 6_suspend.c example does call a function by that name, and the 6_suspend.prx model extraction file contains the definition in the lookup-table. So, this is a little mysterious.

[zhang-cell]

Thank you for such a detailed answer. Do you know why% L is defined in the. PRX file mutex lock(&(count lock)) atomic { count lock == 0 -> count lock = 1 } mutex unlock(&(count lock)) count lock = 0 In the generated Promela model: int count lock; int count; c state "char str[80]" "Local p main" c state "void * arg" "Local p counter" bool Suspended; active proctype p main() { int ctid; L 3: do :: true; Suspended = 1; c code { mutex lock((&( now.count lock))); }; c code { mutex unlock((&( now.count lock))); }; Suspended = 0; goto L 3; :: else; -> break od; goto Return; Return: skip; } active proctype p counter() provided (!Suspended) { int i; L 0: do :: true; c code { mutex lock((&( now.count lock))); }; c code { now.count ++; }; c code { Pp counter->i=0; }; L 1: skip; c code { mutex unlock((&( now.count lock))); }; c code { Pp counter->i=0; }; L 2: skip; goto L 0; :: else; -> break od; goto Return; Return: skip; ; } When I modify the mapping relation to: mutex lock(&(count lock)) spin mutex lock(&(count lock)) mutex unlock(&(count lock)) spin mutex unlock(&(count lock)) The generated Promela model is as shown before. Why?. Only if I will generate the mutex in the Promela model lock(&(count Lock) and mutex unlock(&(count Lock) to spin mutex lock(&(count Lock) and spin mutex unlock(&(count_ Lock) GCC compilation will pass. What's more, do you have any other modx learning methods besides the modex manual?

[nimble-code]

I agree that this is not supposed to work that way. you can fix it by replacing those two mappings in the .prx file with:

mutex_lock(... atomic { count_lock == 0 -> count_lock = 1 } mutex_unlock(... count_lock = 0

[zhang-cell]

According to your prompt, my modified. PRX file is as follows:

%X -a main

%X -n counter

%L

gets(str) hide

thr_ create(... hide

printf(... hide

(i<50000) false

thr_ suspend(ctid) Suspended = 1

thr_ continue(ctid) Suspended = 0

mutex lock(... atomic { count lock == 0 -> count_ lock = 1 }

mutex unlock(... count lock = 0

%P

bool Suspended;

include " modex main.pml "

active proctype p_ counter() provided (!Suspended) {

include " modex counter.pml "

}

%G

maxdepth: 100

shortest: 1

%% The proemla model is as follows: // Generated by MODEX Version 2.11 - 3 November 2017 // Fri Jan 22 20:11:38 PST 2021 from 6_suspend.prx

int count_lock; int count; c_state "char str[80]" "Local p_main" c_state "void * arg" "Local p_counter" bool Suspended; active proctype p_main() { int ctid; L_3: do :: true; Suspended = 1; c_code { mutex_lock((&(now.count_lock))); }; c_code { mutex_unlock((&(now.count_lock))); }; Suspended = 0; goto L_3; :: else; -> break od; goto Return; Return: skip; } active proctype p_counter() provided (!Suspended) { int i; L_0: do :: true; c_code { mutex_lock((&(now.count_lock))); }; c_code { now.count++; }; c_code { Pp_counter->i=0; }; L_1: skip; c_code { mutex_unlock((&(now.count_lock))); }; c_code { Pp_counter->i=0; }; L_2: skip; goto L_0; :: else; -> break od; goto Return; Return: skip; ; }

The results of GCC compilation are as follows:

zkwdl@ubuntu:~/urs/local/bun/Modex-master/Examples$ gcc -o pan pan.c In file included from pan.c:5876:0: pan.m: In function ‘do_transit’: pan.m:28:14: warning: implicit declaration of function ‘mutex_lock’; did you mean ‘spin_mutex_lock’? [-Wimplicit-function-declaration] sv_save(); mutex_lock((&(now.count_lock))); } ^~~~~~ spin_mutex_lock pan.m:64:14: warning: implicit declaration of function ‘mutex_unlock’; did you mean ‘spin_mutex_unlock’? [-Wimplicit-function-declaration] sv_save(); mutex_unlock((&(now.count_lock))); } ^~~~ spin_mutex_unlock /tmp/ccm0kZI7.o: In function do_transit': pan.c:(.text+0x2e96): undefined reference tomutex_lock' pan.c:(.text+0x2f18): undefined reference to mutex_unlock' pan.c:(.text+0x2fe8): undefined reference tomutex_lock' pan.c:(.text+0x3015): undefined reference to `mutex_unlock' collect2: error: ld returned 1 exit status I don't think the modex manual is very comprehensive. Do you have any other learning ways to recommend？

[nimble-code]

there's a new version of the file 6_suspend.prx on github (watch the separation between left and right column in the lookup table)

[zhang-cell]

thank you.Do you know any other way to learn about modex besides the modex manual？

[nimble-code]

there's a short course available on spinroot.com that covers model extraction, but the manual provides the most detailed information -- each application will pose its own challenges, but if you're persistent, you can often solve them

[zhang-cell]

Dear author： I found that when using modex, it's similar to the function in C language. The generated proemla model contains these three Chan, for example: chan ret_p_thread2 = [1] of { pid }; chan exc_cll_p_thread2 = [0] of { pid }; chan req_cll_p_thread2 = [1] of { pid }; I don't quite understand the role of these three chan In the generated proemla function, in addition to the main function, other functions contain the following atomic statements: 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); c_code { Pp_thread2->arg = now.par0_thread2; }; lck_p_thread2 = 0; }; I don't quite understand what this is about？Looking forward to your answer

[nimble-code]

These are parts of the internal encoding of the semantics of Promela specifications. Are you interested in using Modex to extract verification models from C code, or are you interested in implementing a tool that performs a similar fuinction to Modex?

[zhang-cell]

I want to make a simple automation tool, which can automatically generate. PRX file through C program to simply verify some multithreading problems in C. So I need to understand the Promela model generated by modex

[zhang-cell]

Dear author: This is the model extraction of modex case 6： int count_lock; int count; c_state "char str[80]" "Local p_main" c_state "void * arg" "Local p_counter" bool Suspended; active proctype p_main() { int ctid; L_3: do :: true; Suspended = 1; atomic { count_lock == 0 -> count_lock = 1 }; count_lock = 0; Suspended = 0; goto L_3; :: else; -> break od; goto Return; Return: skip; } active proctype p_counter() provided (!Suspended) { int i; L_0: do :: true; atomic { count_lock == 0 -> count_lock = 1 }; c_code { now.count++; }; c_code { Pp_counter->i=0; }; L_1: skip; count_lock = 0; c_code { Pp_counter->i=0; }; L_2: skip; goto L0; :: else; -> break od; goto Return; Return: skip; ; } I think atomic {count -- lock = = 0 - > count Lock = 1} and count_ Lock = 0; does not implement the locking mechanism of the corresponding lock in the C source code, what do you think?

[nimble-code]

why do you believe it's not accurate?

[zhang-cell]

Dear author： Case 6. The operation of locking and unlocking a mutex variable in PRX file is "mutex Lock (..." and "mutex unlock（..." . If there are more than two mutually exclusive variables, how to define the mapping relationship

[nimble-code]

you'd use two different lock variables, like count_lock in the example

[zhang-cell]

If I have four lock variables, should the write mapping be like this? pthread_mutex_lock(... atomic { mutex1 == 0 -> mutex1 = 1 } pthread_mutex_unlock(... mutex1=0 pthread_mutex_lock(... atomic { mutex2 == 0 -> mutex2 = 1 } pthread_mutex_unlock(... mutex2=0 pthread_mutex_lock(... atomic { mutex3 == 0 -> mutex3 = 1 } pthread_mutex_unlock(... mutex3=0 pthread_mutex_lock(... atomic { mutex4 == 0 -> mutex4 = 1 } pthread_mutex_unlock(... mutex4=0 But they don't appear in the Promela model: atomic { mutex2 == 0 -> mutex2 = 1 } It is c_code { spin_mutex_lock((&(now.mutex2))); }; }; Obviously it's not what I want

[nimble-code]

yes, that's how you would do that -- the version that is generated is equivalent, but more efficient