Inquiry regarding CPAChecker deadlock detection feature
29 views
Skip to first unread message
sanjanasai
Dec 11, 2023, 8:17:12 AM12/11/23
to CPAchecker Users
Hello Team,
I am working on verification of multithreaded applications based on C code and focusing on the detection of the deadlock and race conditions in the multithreaded C applications which was backed by your paper "A Light-Weight Approach for Verifying Multi-Threaded
Programs with CPAchecker" , the snippet referring to especially the deadlock detection as attached. Based on the statement, I could not find a command or instructions directly pertaining to the deadlock detection in the tool manual.
Kindly guide me through if there are any features in the tool that can be utilized to directly detect deadlocks or can be built around the existing options and would there be any support from the tool community regarding this.
Programs with CPAchecker" , the snippet referring to especially the deadlock detection as attached. Based on the statement, I could not find a command or instructions directly pertaining to the deadlock detection in the tool manual.
Kindly guide me through if there are any features in the tool that can be utilized to directly detect deadlocks or can be built around the existing options and would there be any support from the tool community regarding this.
Philipp Wendler
Dec 20, 2023, 9:47:57 AM12/20/23
to cpacheck...@googlegroups.com
Dear sanjanasai,
thank you for your interest in CPAchecker!
Am 11.12.23 um 14:10 schrieb sanjanasai:
> I am working on verification of multithreaded applications based on C code
> and focusing on the detection of the deadlock and race conditions in the
> multithreaded C applications which was backed by your paper "A Light-Weight
> Approach for Verifying Multi-Threaded
> Programs with CPAchecker" , the snippet referring to especially the
> deadlock detection as attached. Based on the statement, I could not find a
> command or instructions directly pertaining to the deadlock detection in
> the tool manual.
The observer automaton that is referred to in the paper is in file
"config/specification/deadlock.spc" in the CPAchecker repository.
The best suited deadlock analysis should be
config/deadlock-detection.properties AFAIK, so you will have the best
chance with the following parameters:
-deadlock-detection -spec deadlock
However, please note that the respective parts of CPAchecker are not
under active development currently and not all people involved in that
project are active anymore.
So it may be that you encounter some open issues.
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
thank you for your interest in CPAchecker!
Am 11.12.23 um 14:10 schrieb sanjanasai:
> I am working on verification of multithreaded applications based on C code
> and focusing on the detection of the deadlock and race conditions in the
> multithreaded C applications which was backed by your paper "A Light-Weight
> Approach for Verifying Multi-Threaded
> Programs with CPAchecker" , the snippet referring to especially the
> deadlock detection as attached. Based on the statement, I could not find a
> command or instructions directly pertaining to the deadlock detection in
> the tool manual.
"config/specification/deadlock.spc" in the CPAchecker repository.
The best suited deadlock analysis should be
config/deadlock-detection.properties AFAIK, so you will have the best
chance with the following parameters:
-deadlock-detection -spec deadlock
However, please note that the respective parts of CPAchecker are not
under active development currently and not all people involved in that
project are active anymore.
So it may be that you encounter some open issues.
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
Reply all
Reply to author
Forward
0 new messages