jan@jan-HP-ZBook-15u-G5:~$ spin -search mdev-pre-21910.pl pan.c: In function ‘make_trail’: pan.c:2018:19: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=] 2018 | sprintf(fnm, "%s%d.%s", | ^~ pan.c:2018:16: note: directive argument in the range [1, 2147483647] 2018 | sprintf(fnm, "%s%d.%s", | ^~~~~~~~~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2026:22: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 2026 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2033:21: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=] 2033 | sprintf(fnm, "%s%d.%s", | ^~ pan.c:2033:18: note: directive argument in the range [1, 2147483646] 2033 | sprintf(fnm, "%s%d.%s", | ^~~~~~~~~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2036:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 2036 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c: In function ‘findtrail’: pan.c:1622:22: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=] 1594 | tprefix = "trail"; | ~~~~~~~ ...... 1622 | { sprintf(fnm, "%s.%s", MyFile, tprefix); | ^~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1633:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 1633 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1598:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1598 | { sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1610:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1610 | sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1672:21: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=] 1659 | tprefix = "trail"; | ~~~~~~~ ...... 1672 | { sprintf(fnm, "%s.%s", MyFile, tprefix); | ^~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1676:23: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 1676 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1662:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1662 | { sprintf(fnm, "%s%d.%s", MyFile, whichtrail, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1666:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1666 | sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan:1: invalid end state (at depth 8) pan: wrote mdev-pre-21910.pl.trail (Spin Version 6.4.9 -- 17 December 2018) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 44 byte, depth reached 31, errors: 1 32 states, stored 0 states, matched 32 transitions (= stored+matched) 2 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.002 equivalent memory usage for states (stored*(State-vector + overhead)) 0.288 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage pan: elapsed time 0 seconds jan@jan-HP-ZBook-15u-G5:~$ spin -p -t mdev-pre-21910.pl Starting kill with pid 1 1: proc 0 (:init::1) mdev-pre-21910.pl:59 (state 1) [(run kill())] Starting bf_kill with pid 2 2: proc 0 (:init::1) mdev-pre-21910.pl:59 (state 2) [(run bf_kill())] Starting monitor with pid 3 3: proc 0 (:init::1) mdev-pre-21910.pl:59 (state 3) [(run monitor())] 4: proc 3 (monitor:1) mdev-pre-21910.pl:55 (state 1) [assert((count!=2))] 4: proc 3 (monitor:1) mdev-pre-21910.pl:55 (state 2) [assert((count2!=2))] 4: proc 3 (monitor:1) mdev-pre-21910.pl:55 (state 3) [assert((count3!=2))] 5: proc 3 terminates 6: proc 2 (bf_kill:1) mdev-pre-21910.pl:42 (state 1) [((flag!=1))] 6: proc 2 (bf_kill:1) mdev-pre-21910.pl:42 (state 2) [flag = 1] 7: proc 2 (bf_kill:1) mdev-pre-21910.pl:43 (state 4) [count2 = (count2+1)] 8: proc 1 (kill:1) mdev-pre-21910.pl:29 (state 1) [((flag2!=1))] 8: proc 1 (kill:1) mdev-pre-21910.pl:29 (state 2) [flag2 = 1] 9: proc 1 (kill:1) mdev-pre-21910.pl:30 (state 4) [count3 = (count3+1)] spin: trail ends after 9 steps #processes: 3 aborter = 0 count = 0 count2 = 1 count3 = 1 flag = 1 flag2 = 1 9: proc 2 (bf_kill:1) mdev-pre-21910.pl:45 (state 7) 9: proc 1 (kill:1) mdev-pre-21910.pl:32 (state 7) 9: proc 0 (:init::1) mdev-pre-21910.pl:60 (state 5) 4 processes created Analysis: bf_kill() and kill() are in mutex deadlock as line 45 trying to lock thd->LOCK_thd_data but kill() is holding it and kill() line 33 is trying to lock lock_sys->mutex but bf_kill() is holding it. This is exactly the mutex deadlock MDEV-21910 was trying to fix and managed to fix one scheduling of kill() and bf_kill() but not all.