Bug #682

barrier is not cleaned up correctly

Added by Alfons Laarman over 7 years ago. Updated over 6 years ago.

Status:AssignedStart date:08 Dec 2012
Priority:NormalDue date:
Assignee:Stefan Blom% Done:

0%

Category:toolsSpent time:-
Target version:ltsmin-2.1

Description

For correct barrier deallocation see http://locklessinc.com/articles/barriers/

~/ltsmin-hre/src/pins2lts-mc/dve2lts-mc ~/tests/dve/ltl-new/elevator2.3.prop4.dve2C --threads=48 --state=cleary-tree
dve2lts-mc: Precompiled divine module initialized
dve2lts-mc( 0/48), * error *: Cleary tree not supported in combination with error trails or the MCNDFS algorithms.
  • segmentation fault ***
Please send information on how to reproduce this problem to:

along with all output preceding this message.
In addition, include the following information:
Package: ltsmin 1.8
Stack trace:
  • segmentation fault ***

Please send information on how to reproduce this problem to:

along with all output preceding this message.
In addition, include the following information:
Package: ltsmin 1.8
Stack trace:

History

#1 Updated by Alfons Laarman over 7 years ago

  • Status changed from New to Assigned
  • Assignee changed from Alfons Laarman to Stefan Blom
  • Target version changed from ltsmin-2.0 to ltsmin-2.1

#2 Updated by Alfons Laarman over 6 years ago

ask stefan.
resolved in next?

Also available in: Atom PDF