Increasing the verbosity of Armus

Armus uses the logging infrastructure of Java, so you can increase its verbosity by using the parameter -Djava.util.logging.config.file=logging.properties.

For example, to include all messages into a file named armus.log, then instead of running java YourApp you can do

java -Djava.util.logging.config.file=logging.properties YourApp

where the contents of file logging.properties are:

# Define the behaviour of logging to a file and logging to the console
handlers= java.util.logging.FileHandler, java.util.logging.ConsoleHandler

# Default global logging level.
# This specifies which kinds of events are logged across
# all loggers. For any given facility this global level
# can be overriden by a facility specific level
# Note that the ConsoleHandler also has a separate level
# setting to limit messages printed to the console.
.level= ALL

# default file output is in user's home directory. When logging to a file,
# include ALL messages
java.util.logging.FileHandler.pattern = armus.log
java.util.logging.FileHandler.level = ALL
java.util.logging.FileHandler.formatter = java.util.logging.SimpleFormatter

# Limit the message that are printed on the console to INFO and above.
java.util.logging.ConsoleHandler.level = INFO
java.util.logging.ConsoleHandler.formatter = java.util.logging.SimpleFormatter

Change the verification strategy

• armus.strategy: you can choose AVOIDANCE for the deadlock avoidance algorithm, DETECTION for a deadlock detection algorithm, and DETECTION2 for an alternative deadlock detection algorithm.
• armus.sharedBuffer: you can choose HASH for using the ConcurrentHashMap backend, and QUEUE for using the ConcurrentLinkedQueue backend. Only works with the DETECTION2 backend.
• armus.detection.delay: specify when the deadlock detection algorithm kicks in. Only available for strategies DETECTION and DETECTION2.
• armus.detection.period: specify the period in which the deadlock detection algorihtm runs. Only available for strategies DETECTION and DETECTION2.
• armus.garbageCollection.delay: specify when the edge garbage collection kicks in. Only available for strategy DETECTION.
• armus.garbageCollection.period: specify the period in which the edge garbage collection runs. Only available for strategy DETECTION.

For example, the fastest verification algorithm is strategy DETECTION2, you can make the detection occur very seldom (every 2 seconds). So, instead of running java YourApp you do

java -Darmus.detection.period=2000 -Darmus.strategy=DETECTION2 YourApp