Add Owicki-Gries annotations - #783

Draft

maul-esel wants to merge 576 commits into

devfrom

wip/dk/empire2-owicki

This pull request is big! We're only showing the most recent 250 commits

Commits on Feb 9, 2024

Commits on Feb 14, 2024

hacky support for auxiliary variables in proofs (ghost variables)
maul-esel
committed
d9a5a8a
fix compilation error
maul-esel
committed
575ffb0
add TODO
maul-esel
committed
83b452d
Merge branch 'dev' into wip/dk/empire-owicki
maul-esel
committed
50cfd79
add ghost variable workaround in CACSL2BoogieBacktranslator
maul-esel
committed
d925da4
unpetrify ICFG locations
maul-esel
committed
0b9f583
fix WitnessGhostDeclaration: allow multiple declarations
maul-esel
committed
b505a50

Commits on Feb 20, 2024

two fixes for ghost mirror variables
maul-esel
committed
cfc1b93

Commits on Feb 25, 2024

extended benchmark file

maul-esel
authored and
danieldietsch
committed
80210a2

Commits on May 1, 2024

Commits on May 2, 2024

Only add successor to territory if they are part of the same thread
matthiaszumkeller
committed
3b264fb

Commits on May 8, 2024

Add new EmpireValidityChecker that checks the current validity definition
matthiaszumkeller
committed
7ba8962

Commits on May 9, 2024

Update enables function to new definition and some refactoring
matthiaszumkeller
committed
2695038

Commits on Jun 3, 2024

Add examples to test the algorithm
matthiaszumkeller
committed
213becc

Commits on Jun 4, 2024

Add some handwritten empires for the examples
matthiaszumkeller
committed
95101ed

Commits on Jun 5, 2024

Add some more empires and a test for a race between two threads
matthiaszumkeller
committed
0f6369b
Add empire for thread-race
matthiaszumkeller
committed
f8da360
Fix wrong accepting place in data-race
matthiaszumkeller
committed
eb21afa

Commits on Jun 6, 2024

Add client-server example with choices between different threads
matthiaszumkeller
committed
e8ed844

Commits on Jun 7, 2024

implement new structure of Owicki-Gries annotations
maul-esel
committed
b978666

Commits on Jun 11, 2024

Commits on Jun 13, 2024

Commits on Jun 17, 2024

Change symbolic execution to first iterate over all extending transitions
matthiaszumkeller
committed
34c12f5

Commits on Jun 21, 2024

Add code for federation computation
matthiaszumkeller
committed
a751118
Fix bug with other proof places for federation
matthiaszumkeller
committed
99dfd3a

Commits on Aug 15, 2024

Product automata and some refinements of bridge pairs
matthiaszumkeller
committed
9fad1a3

Commits on Aug 16, 2024

Fix union, bystander handling and empire of client-server-choice example
matthiaszumkeller
committed
35bc246

Commits on Aug 18, 2024

Add post processing without recursion step
matthiaszumkeller
committed
39c13a5

Commits on Aug 21, 2024

Fix bug in EmpireValidityCheck
matthiaszumkeller
committed
d0a4869

Commits on Aug 22, 2024

Fix bug in empire validity and important bridge detection
matthiaszumkeller
committed
1974e5b

Commits on Aug 26, 2024

re-enable assert for evaluation
maul-esel
committed
ef1bd5d
prepare evaluation
maul-esel
committed
3c0b89a

Commits on Aug 27, 2024

Store successors of bridges that violate the bystanders condition
matthiaszumkeller
committed
0d4be59

Commits on Aug 28, 2024

Set log level to error
matthiaszumkeller
committed
c2784f4

Commits on Nov 7, 2024

Add new symbolic execution and Bridge code and remove Federation
matthiaszumkeller
committed
9ec5ed1
pin jdk and maven versions
maul-esel
committed
db85409

Commits on Nov 20, 2024

Commits on Nov 29, 2024

remove unnecessary parameters from EmpireValidityCheck
maul-esel
committed
cf8d64e
Remove necessity for law place in enabledTransitions
matthiaszumkeller
committed
60499b3
Remove unnecessary code
matthiaszumkeller
committed
c194c01
PetriOwickiGries: support both kinds of empire computations
maul-esel
committed
a7d9519
Merge branch 'wip/dk/empire-owicki' into wip/dk/empire2-owicki
maul-esel
committed
5e9e41d
Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
c09e161
remove accidentally re-added, obsolete class InductivityCheck
maul-esel
committed
8a39dab
EmpireAnnotationParser: remove obsolete unused regular expressions
maul-esel
committed
07b837b

Commits on Nov 30, 2024

undo statistics changes that broke StatisticsAggregator
maul-esel
committed
205f48a
remove unused function
maul-esel
committed
bb222c9
remove TraceAbstraction dependency from Library-TraceCheckerUtilsTest
maul-esel
committed
ef861b4
move Owicki-Gries code to Library-Proofs
maul-esel
committed
5212a00
move Owicki-Gries tests into new Library-ProofsTest project
maul-esel
committed
89f8c74
use IFloydHoareAnnotation type instead of Map
maul-esel
committed
1cd1084
OwickiGriesTestSuite: add timeout for long-running tests
maul-esel
committed
89045fd
CrownConstruction: respect toolchain timeout
maul-esel
committed
a54e3f0
remove some unused code
maul-esel
committed
0baa7e1

Commits on Dec 2, 2024

add utility method for initial Marking
maul-esel
committed
8818335
let OwickiGriesAnnotation implement IProof
maul-esel
committed
a80a329
include IPossibleInterferences inside OwickiGriesAnnotation
maul-esel
committed
ce709ff
TransformFloydHoareAnnotation: support default predicate
maul-esel
committed
214e4bd
work on backtranslating proofs and integrating with IProofProducer
maul-esel
committed
5181e69
Add option to construct Empire without PlacesCoRelation
matthiaszumkeller
committed
2f9e4e3
add proof production support to CegarLoopForPetriNets
maul-esel
committed
c6ee139

Commits on Dec 3, 2024

Commits on Dec 4, 2024

fix an NPE
maul-esel
committed
8e265c0

Commits on Dec 5, 2024

Commits on Dec 7, 2024

Add hash() for GraphNode and use only Triples during Empire computation
matthiaszumkeller
committed
34c0d17

Commits on Feb 6, 2025

Add validity check for disjunctive definition
matthiaszumkeller
committed
ffabcac

Commits on Feb 13, 2025

Remove PostProcessing from EmpireComputation
matthiaszumkeller
committed
83c35f9

Commits on Feb 21, 2025

add TODO
maul-esel
committed
e98a6ab
outline for empire automaton implementation
maul-esel
committed
8c7dec6

Commits on Feb 26, 2025

Remove htc and implication checker from EmpireComputation and fix but in algorithm
matthiaszumkeller
committed
55e69d0

Commits on Mar 8, 2025

Add first version of Empire Automaton construction
matthiaszumkeller
committed
faeeadf

Commits on Mar 9, 2025

Add first version of Automaton validity check
matthiaszumkeller
committed
00b6d89
Add check for accepting places to validity check
matthiaszumkeller
committed
dfead2a

Commits on Mar 10, 2025

Add Testsuite class for Empire Automaton validity
matthiaszumkeller
committed
2da9873
Remove unnecessary computation
matthiaszumkeller
committed
f1a1cfa

Commits on Mar 14, 2025

minor fix
maul-esel
committed
f61efc6
updated og-benchmark-generator.xml for evaluation

maul-esel
authored and
danieldietsch
committed
5810587
fix no-overflow setting; increase timeout

maul-esel
authored and
danieldietsch
committed
018ac6c

Commits on Mar 16, 2025

prepare O/G proof generation benchmarking

maul-esel
authored and
danieldietsch
committed
070570e

Commits on Mar 18, 2025

Add first attempt of OG construction from Empire Automaton
matthiaszumkeller
committed
a2e4463

Commits on Mar 19, 2025

Add ProofProduceTest for Empire Automata to OG
matthiaszumkeller
committed
b0fc308

Commits on Mar 20, 2025

Commits on Mar 21, 2025

prepare evaluation

maul-esel
authored and
danieldietsch
committed
e5935f3
remove obsolete runconfigs
maul-esel
committed
375476c
OwickiGriesTestSuite: lift timeout when running via benchexec
maul-esel
committed
ad8bc2a
minor simplifications
maul-esel
committed
478e9be

Commits on Mar 26, 2025

Add class to compute automata statistics
matthiaszumkeller
committed
aa94c20

Commits on Mar 27, 2025

add example with non-executable transitions
maul-esel
committed
7d34fd4
extend statistics slightly
maul-esel
committed
6093dce
fix timer statistics: redundant specification of unit
maul-esel
committed
cb7e8b8
OGProofProducerTest: print statistics
maul-esel
committed
d9deecd
OwickiGriesTestSuite: actually set LOG_LEVEL (otherwise defaults to DEBUG)
maul-esel
committed
690af1f
Add regions per territory and places per region statistics
matthiaszumkeller
committed
b08565a

Commits on Mar 30, 2025

consistently use declareCounter()
maul-esel
committed
b186fb2

Commits on Mar 31, 2025

Add first version of OG Conjunction and headers
matthiaszumkeller
committed
c50bab0
Add ProofProducer for OG Conjunction
matthiaszumkeller
committed
09491b9

Commits on Apr 1, 2025

Add transitions to true to proof automata
matthiaszumkeller
committed
785034a
Fix mistake
matthiaszumkeller
committed
4f1210f
Remove OG logging
matthiaszumkeller
committed
121d798

Commits on Apr 3, 2025

Commits on Apr 7, 2025

add three new test cases
maul-esel
committed
0b50dff

Commits on Apr 13, 2025

remove empty lines
maul-esel
committed
c18b1fd
add more test cases with loops and locks
maul-esel
committed
83ad567

Commits on May 6, 2025

begin setting up test suite for expected O/G annotations
maul-esel
committed
445630f
add documentation
maul-esel
committed
927519a
OwickiGriesValidityCheck: fix logging message
maul-esel
committed
d425126

Commits on May 8, 2025

Commits on May 10, 2025

optimizations: cache Region::hashCode, Territory::getPlaces
maul-esel
committed
9683d8c
additional logging and statistics
maul-esel
committed
527d3a4
minor fix
maul-esel
committed
825cbc7
add (hacky) support for trivial focus
maul-esel
committed
2a7140b
EmpireAutomaton.State: cache hash code for performance
maul-esel
committed
c98dc12
add test case for very slow separate-Empire computation
maul-esel
committed
826fbc5

Commits on May 11, 2025

Commits on May 12, 2025

Commits on May 13, 2025

Add assertion for error places
matthiaszumkeller
committed
272fa48

Commits on May 15, 2025

begin modularity statistics (hacky version)
maul-esel
committed
b380eac
EmpireAutomaton: simplifications, small improvements
maul-esel
committed
8602faf

Commits on May 18, 2025

Add test program that showcases the error in empire graph construction
matthiaszumkeller
committed
8e07644

Commits on May 21, 2025

Add new Single Empire Automaton class to solve safety problems regarding single proof automata construction
matthiaszumkeller
committed
650047d

Commits on May 26, 2025

Commits on May 28, 2025

Add Region subtype with stored transition and adjust other classes to new Region and Territory implementation
matthiaszumkeller
committed
8516750

Commits on May 31, 2025

Add Connected Region intersection and Product construction
matthiaszumkeller
committed
1c0c1e6

Commits on Jun 1, 2025

Add Product construction and Legal focus to OG
matthiaszumkeller
committed
842c847

Commits on Jun 5, 2025

Add counterexample for region intersection
matthiaszumkeller
committed
523d026

Commits on Jun 9, 2025

Only use joint transitions for region intersection
matthiaszumkeller
committed
20b65ce

Commits on Jun 11, 2025

Add new legal focus computation
matthiaszumkeller
committed
9966ef0

Commits on Jun 12, 2025

Commits on Jun 13, 2025

Refactoring of empire automata and legal focus
maul-esel
committed
aaa7e6a

Commits on Jun 15, 2025

Implement cooperative version of inductive-false for legal focus
matthiaszumkeller
committed
eb18dfb

Commits on Jun 16, 2025

Commits on Jun 18, 2025

Change States from triples to pair
matthiaszumkeller
committed
650fd22

Commits on Jun 19, 2025

minor code style fix
maul-esel
committed
3081cf6
test setup improvements
maul-esel
committed
f4aa81c
update benchmark setup
maul-esel
committed
f5de5c7

Commits on Jun 20, 2025

add missing declaration of Floyd-Hoare statistics
maul-esel
committed
cff45d0

Commits on Jun 21, 2025

EmpireAutomaton: technical optimizations
maul-esel
committed
ec93230
EmpireAutomaton: further optimizations
maul-esel
committed
1e7b5de

Commits on Jun 22, 2025

Territory: improve efficiency of getBystanders(), getPlaceRegion() etc
maul-esel
committed
f93ca2f

Commits on Jun 24, 2025

CC fixes
maul-esel
committed
e0d1053
Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
0cad94d

Commits on Jun 27, 2025

Owicki-Gries tests: export and parse possible interferences
maul-esel
committed
e8a2d85

Commits on Jun 28, 2025

fix parameters for O/G benchmark generation

maul-esel
authored and
danieldietsch
committed
0ff3bbf

Commits on Jun 30, 2025

Commits on Jul 2, 2025

Commits on Jul 3, 2025

update table definition
maul-esel
committed
a729581

Commits on Oct 13, 2025

O/G proof producers: pass on-demand implementation of difference
maul-esel
committed
ca75bc8

Commits on Dec 17, 2025

Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
4b38ec5
fix build error: InvariantResult now expects invariant string
maul-esel
committed
484c1b2
TraceAbstractionStarter: remove some unnecessary casts
maul-esel
committed
6ee76ab

Commits on Mar 23, 2026

Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
8877748

Commits on Apr 29, 2026

Commits on Apr 30, 2026

skip proof unpetrification if there is no proof
maul-esel
committed
2b60b3d

Commits on May 4, 2026

add support for ghost updates at join statements
maul-esel
committed
ecb8f24
prepare evaluation
maul-esel
committed
415509e

Commits on May 5, 2026

add example from POPL'26 paper as O/G test
maul-esel
committed
65df15d

Commits on May 7, 2026

Commits on May 28, 2026

Commits on May 29, 2026

Owicki-Gries proofs: reorganise package structure
maul-esel
committed
107e2f2
delete some unused code (O/G proof producers no longer need the unfolding)
maul-esel
committed
eb55be9
OwickiGriesTestSuite: small simplification
maul-esel
committed
a249742
fix compile error introduced by eb55be9f
maul-esel
committed
7354a6d
remove some no-longer needed dependencies from test projects
maul-esel
committed
a1f4ea5
remove outdated comment
maul-esel
committed
c7bd7d5
remove an unused method
maul-esel
committed
9c5b796

Commits on Jun 1, 2026

cleanup & document "~ghost~" variable name prefix handling
maul-esel
committed
5aba76b
rename OwickiGriesConstruction (add "Naive") and move auxiliary method
maul-esel
committed
9262eca
O/G: move result & ICFG annotation creation to auxiliary method
maul-esel
committed
1d983aa
O/G: rename *EmpireToOG classes, add some documentation
maul-esel
committed
a5da9da
remove unused and dangerous method
maul-esel
committed
fed2a73
fix compile error introduced by 1d983aa967
maul-esel
committed
2705c1d
renaming: remove "Automaton" from empires
maul-esel
committed
986eab7

Commits on Jun 19, 2026

Commits on Jun 21, 2026

containsNotOnlyISLPredicate: Return true if there are not only ISLPredicate in the region so that the comparator prefers regions with only ISLPredicates
matthiaszumkeller
committed
a9239f0

Commits on Jun 25, 2026

Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
7129b4d

Commits on Jul 28, 2026

fix GhostUpdate::combine: did not actually implement combination
maul-esel
committed
3705400

Commits on Jul 29, 2026

Commits on Aug 12, 2026

Commits on Aug 15, 2026

Merge branch 'dev' into wip/dk/empire2-owicki
maul-esel
committed
a3e33aa
fix O/G test build
maul-esel
committed
7bf821c