deadlock-detection.properties

# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# ########################################################################
# This configuration uses the BDD-analysis (or value-analysis) to detect
# deadlock in concurrent programs.
# The current internal limit for the number of parallel threads is 5.
# We use CFA-cloning to have separate CFAs for each thread.
# ########################################################################

#include bddAnalysis-concurrency.properties

# Our implementation of localAccessLocks is unsound in case of deadlocks,
# e.g. in a case where two threads are analysed that have the following form:
# thread1: "pthread_lock(&glob_1); int local; pthread_lock(&glob_2)" and
# thread2: "pthread_lock(&glob_2); int local; pthread_lock(&glob_1)".
# Then we never reach the state (2,2), where both outgoing edges require a lock.
cpa.threading.useLocalAccessLocks=false