Spinroot

faisal2000

Member

Registered: 2010-11-29

Posts: 9

example program in C language which have deadlock

can any body send the example program in C which have dead lock error and can be identify by using SPIN. thanks

awesan

Member

Registered: 2011-04-30

Posts: 45

Re: example program in C language which have deadlock

I don't have one. But, you can write a simple one that does the following: Proc-1 acquires mutex-A and mutex-B. Proc-2 acquires mutex-B and mutex-A. If you try to model this in SPIN, yes, SPIN indeed will throw an error when you verify the model for safety (and you can replay the error trail to see - where two processes are - causing the deadlock). If your intent is not to use embedded C or model extraction from C program, you can directly model this in PROMELA and try SPIN on it.

Last edited by awesan (2012-01-12 19:24:14)