[ 0:01] compiling /home/xrockai/src/divine/nightly/test/demo/1.deadlock.c [ 0:01] states per second: 155.565 [ 0:23] state count: 1100 [ 0:23] mips: 0.16 [ 0:23] [ 0:28] error found: yes [ 0:28] error trace: | [ 0:28] [0] 0: locking mutex 1 [ 0:28] [0] 0: locking mutex 2 [ 0:28] [1] 1: locking mutex 2 [ 0:28] [1] 1: locking mutex 1 [ 0:28] (1) FAULT: Deadlock: mutex cycle closed, circular waiting [ 0:28] [1] FATAL: locking error in userspace [ 0:28] [ 0:28] stack 2: [ 0:29] - symbol: __dios::_InterruptMask::Without::Without(__dios::_InterruptMask&) [ 0:29] location: /divine/include/libc/include/sys/interrupt.h:42 [ 0:29] - symbol: _mutex_lock(__dios::_InterruptMask&, pthread_mutex_t*, bool) [ 0:29] location: /divine/include/libc/include/sys/interrupt.h:77 [ 0:29] - symbol: pthread_mutex_lock [ 0:29] location: /divine/src/libc/functions/sys/pthread.cpp:866 [ 0:29] - symbol: main [ 0:29] location: /home/xrockai/src/divine/nightly/test/demo/1.deadlock.c:31 [ 0:29] - symbol: _start [ 0:29] location: /divine/src/libc/functions/sys/start.cpp:76 [ 0:29] active stack: [ 0:29] - symbol: void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) [ 0:29] location: /divine/include/dios/core/fault.hpp:187 [ 0:29] - symbol: __dios_fault [ 0:29] location: /divine/src/libc/functions/sys/fault.c:25 [ 0:29] - symbol: _mutex_lock(__dios::_InterruptMask&, pthread_mutex_t*, bool) [ 0:29] location: /divine/src/libc/functions/sys/pthread.cpp:754 [ 0:29] - symbol: pthread_mutex_lock [ 0:29] location: /divine/src/libc/functions/sys/pthread.cpp:866 [ 0:29] - symbol: thr1 [ 0:29] location: /home/xrockai/src/divine/nightly/test/demo/1.deadlock.c:14 [ 0:29] - symbol: __pthread_entry [ 0:29] location: /divine/src/libc/functions/sys/pthread.cpp:462 [ 0:29] a report was written to verify.out [ 0:29] [ 0:39] ^ —————. —.— . . —.— . . .————— . . [ 0:39] ——— | | | | | | |\ | | | | [ 0:39] —(o)— | | | | | | | \ | |———— '————| [ 0:39] ——————— | | | \ / | | \| | | [ 0:39] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:39] [ 0:39] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:39] traced states: #1 #2 #3 #4 #5 #6 #7 #8 #9 #10 #11 #12 #13 #14 #15 #16 #17 #18 #19 #20 #21 #22 #23 #24 #25 #26 #27 #28 #29 #30 #31 #32 #33 #34 #35 #36 #37 #38 #39 #40 #41 #42 #43 #44 #45 #46 #47 #48 #49 #50 #51 #52 #53 #54 #55 #56 #57 #58 #59 #60 #61 #62 #63 [ 0:44] trace: [ 0:44] T: [0] 0: locking mutex 1 [ 0:44] T: [0] 0: locking mutex 2 [ 0:44] T: [1] 1: locking mutex 2 [ 0:44] T: [1] 1: locking mutex 1 [ 0:44] # active threads: 0:0 [0:1] [ 0:44] T: (1) FAULT: Deadlock: mutex cycle closed, circular waiting [ 0:44] T: [1] FATAL: locking error in userspace [ 0:44] # executing void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) at /divine/include/dios/core/fault.hpp:187 [ 0:44] # NOTE: $frame in __dios_fault [ 0:44] > backtrace [ 0:44] void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) at /divine/include/dios/core/fault.hpp:187 [ 0:44] __dios_fault at /divine/src/libc/functions/sys/fault.c:25 [ 0:44] _mutex_lock(__dios::_InterruptMask&, pthread_mutex_t*, bool) at /divine/src/libc/functions/sys/pthread.cpp:754 [ 0:44] pthread_mutex_lock at /divine/src/libc/functions/sys/pthread.cpp:866 [ 0:44] thr1 at /home/xrockai/src/divine/nightly/test/demo/1.deadlock.c:14 [ 0:44] __pthread_entry at /divine/src/libc/functions/sys/pthread.cpp:462 [ 0:44] # executing void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) at /divine/include/dios/core/fault.hpp:187 [ 0:44] # NOTE: $frame in __dios_fault [ 0:44] spec: pthread_mutex_lock