#429 complete static deadlock detection (SDD)

[Rainer Müller]

last state in ticket #390

• static deadlock detection switched off by default in the prl-script
• the export of the control deadlock control flow graph has some problems with some test cases (loops and other stuff)
• the static analyzer already works with multiple modules
• export of identifiers with separate namespaces not tested yet

[Anonymous]

next issues in export for static analyzer:

• export of local procedures or tasks with deadlock operation with decoration for unique identification: filename+namespace+name
• export of global procedures or tasks with deadlock operation as namespace+name
• remove local procedures without deadlock operation from the export
• export global procedures/tasks without deadlock operation as namespace+name and marker nodeadlockoperations
• export local semaphores, bolts as filename+namespace+name
• export global semaphores, bolts as namespace+name

after these changes, modify static analyzer:

• simplify the global control flow graph be removing all calls to procedures without deadlock relevant operations
• remove tasks and procedures without deadlock relevant operations from the CFG
• generate graph complexity informations (#nodes, #transitions) for each task and procedure

[Rainer Müller]

it would be better for understanding if all task/proc/sema/... identifiers obtain a new tag module for a unique identification cross over different modules

The staticAnalyzer must become aware of the tag and must regard this when an object id referenced.
If we are certain that the IMC runs before the staticAnalyzer, we may rely on a correct application.

Attention: The name of the module is not regarded by the staticAnalyzer up to now

[Anonymous]

The difference of node-label and node-id is not clear. If several statements are in the same line, the column index must be used.

1. It would be helpful to modify the AbstractControlFlowGraphNode to used a SourceLocation (sourceFilename, includefFlename, line, column). The attribute nodeId should be removed, since the nodeId is defined by the SourceLocation.
2. the methods getLabel(),getInfo() and getNodeLabel() should become unified
3. The UnkonwnStatement should become renamed to IrrelevantStatement and the nodeId should also become removed, since the the SourceLocation was inherited from AbstractControlFlowGraphNode.
4. The export of the DOT-file must use the SourceLocation as node id for the DOT-file.
5. Names of tasks, procedures, semaphores, bolts must be treated with a prefix, which is ether the module-name or the SourceLocation for non global elements. This may be solved by replacing the objects name as String by a reference to the objects definition.
6. The compiler currently exports procedures with a marker whether they are deadlock relevant. Procedure calls to deadlock irrelevant procedures should become removed from the ApplicationControlFlowGraph. This must be repeated withe all procedures which are not deadlock relevant because of removed procedure calls.
7. Tasks which are not deadlock relevant should be removed from the exported control flow graph during the export of the CFG for the SDD

*to be extended and modified *

[Rainer Müller]

update:

• SourceLocation is used to identify declarations and operations
• local procedures without deadlock relevant operations are no longer exported by the compiler
• procedures which may run into a endless loop are exported to the SDD

open issues:

• global procedures without deadlock relevant operations should become removed by the SDD
• error messages should be more readable due to the use of SourecLocation
• warning for sequential RELEASE, FREE, LEAVE should be removed

[Rainer Müller]

names of identifiers became simplified in error messages.
E.g. pc_buffer.prl:7:9::freeonly freeis used if no other object with the same name exists.

If there are other declarations with the same name the
pc_buffer.prl:7:9::free becomes replaced by free (defined at pc_buffer.prl:7:9)

If the definition is located in an included file, the result looks like
free (defined at pc_buffer1.prl:7:./pc_buffer1.inc:2:9)
which means that free was defined in line 2 and column 9. in pc_buffer1.inc, which was included from pc_buffer1.prl in line 7.

still open issues:

• global procedures without deadlock relevant operations should become removed by the SDD
• warning for sequential RELEASE, FREE, LEAVE should be removed
• all tests from the thesis of Jan Knoblauch should be verified to show proper results

[Rainer Müller]

The tests in the thesis of Jan showed that there were some misunderstandings of the usage of semaphore and bolt operations

1. a sequential REQUEST on the same semaphore may be useful. Thus
2. sequential operations on different semaphores or bolts without other operations in between should be combined for code simplification. This is ok for the locking operations. The unlocking operations may affect starvation situations, if the operations are not executed without interruption.
3. RESERVE, FREE, ENTER, LEAVE with duplicate use of a semaphore in the list cannot be resolved by another task, since RESERVE and ENTER require all BOLTs to be free, otherwise the task is blocked eternally.

This concerns the error messages in the static deadlock detection.

The runtime system is expected to emit a BoltStateSignal.

The OpenPEARL language report states that RESERVE b,b; will never succeed. Maybe this is wrong and should be changed towards the BoltStateSignal.

Te BOLT operations should lock and unlock in the same block level of the source code. Other usage should deliver a warning. This was accepted in the discussion from 2029-02-09