Code

Side-effectful Nontermination#772

Code

Open

ThomasHaas wants to merge 38 commits intodevelopmenthernanponcedeleon/Dat3M:developmentfrom non-terminationhernanponcedeleon/Dat3M:non-terminationCopy head branch name to clipboard

+4,064-1,240

Commits

Commits on Nov 7, 2024

• Added new NonTerminationEncoder that can reason over side-effectful non-termination

  ThomasHaas

  committed
  48e40bf

  Copy full SHA for 48e40bf

• Added 5 new side-effectful nontermination tests.

  Show description for 78caf43
  ThomasHaas

  committed
  78caf43

  Copy full SHA for 78caf43

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  112ed0c

  Copy full SHA for 112ed0c

• Updated the new Nontermination tests, mainly to be (almost) race-free

  Show description for 2150e68
  ThomasHaas

  committed
  2150e68

  Copy full SHA for 2150e68

Commits on Nov 10, 2024

• Added new NonTerminationEncoder that can reason over side-effectful non-termination

  

  ThomasHaas

  authored and

  hernanponcedeleon

  committed
  d663e54

  Copy full SHA for d663e54

• Added 5 new side-effectful nontermination tests.

  Show description for 5257846
  

  ThomasHaas

  authored and

  hernanponcedeleon

  committed
  5257846

  Copy full SHA for 5257846

• Updated the new Nontermination tests, mainly to be (almost) race-free

  Show description for 5200c69
  

  ThomasHaas

  authored and

  hernanponcedeleon

  committed
  5200c69

  Copy full SHA for 5200c69

Commits on Nov 11, 2024

• Merge remote-tracking branch 'origin/non-termination' into non-termination

  ThomasHaas

  committed
  84d91d2

  Copy full SHA for 84d91d2

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  57fb307

  Copy full SHA for 57fb307

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  3312d61

  Copy full SHA for 3312d61

Commits on Nov 21, 2024

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  90ce2b8

  Copy full SHA for 90ce2b8

Commits on Dec 9, 2024

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  8d0ca46

  Copy full SHA for 8d0ca46

Commits on Dec 10, 2024

• Minor changes to nontermination_weak.c benchmark

  ThomasHaas

  committed
  768b090

  Copy full SHA for 768b090

• Added new StateSnapshot event for instrumentation of non-termination detection: this removes a wrong verdict related to SCCP removing the whole loop body.

  Show description for 0e852a1
  ThomasHaas

  committed
  0e852a1

  Copy full SHA for 0e852a1

Commits on Jan 5, 2025

• Add NonUniformBarrier test

  hernan-poncedeleon

  committed
  6f5d60b

  Copy full SHA for 6f5d60b

Commits on Jan 7, 2025

• Enable more forward progress tests

  hernan-poncedeleon

  committed
  bda6540

  Copy full SHA for bda6540

Commits on Jan 8, 2025

• Add test for store fairness

  hernan-poncedeleon

  committed
  798eefa

  Copy full SHA for 798eefa

Commits on Jan 10, 2025

• Add safe and unsafe NonUniformBarrier tests

  hernan-poncedeleon

  committed
  2c683e9

  Copy full SHA for 2c683e9

Commits on Jan 15, 2025

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  a2cb70e

  Copy full SHA for a2cb70e

• Added handling of fairness for RMWStoreExclusive (WIP)

  Show description for e300c5b
  ThomasHaas

  committed
  e300c5b

  Copy full SHA for e300c5b

• Merge remote-tracking branch 'origin/non-termination' into non-termination

  ThomasHaas

  committed
  752a68c

  Copy full SHA for 752a68c

Commits on Feb 3, 2025

• Update expected CADP results using the weak fairness variants

  hernan-poncedeleon

  committed
  40624e9

  Copy full SHA for 40624e9

• Add filter spec to spirv tests (#795)

  

  natgavrilenko

  authored and

  ThomasHaas

  committed
  96e6bed

  Copy full SHA for 96e6bed

• Use alignment information in VisitorLlvm.visitAllocaInst() (#796)

  

  hernanponcedeleon

  authored and

  ThomasHaas

  committed
  1f60258

  Copy full SHA for 1f60258

Commits on Feb 6, 2025

• Draft of improved NonTerminationEncoder (WIP)

  ThomasHaas

  committed
  8006d5b

  Copy full SHA for 8006d5b

• Fixed bug due to non-unique variable names in encoding.

  ThomasHaas

  committed
  78a11ba

  Copy full SHA for 78a11ba

• - Renamed NonTerminationEncoderNew to NonTerminationEncoder (removed old version)

  Show description for 7cef8eb
  ThomasHaas

  committed
  7cef8eb

  Copy full SHA for 7cef8eb

Commits on Feb 7, 2025

• Added NonterminationDetection pass to instrument detection of complex (asymmetric) non-termination.

  Show description for d0a2a3a
  ThomasHaas

  committed
  d0a2a3a

  Copy full SHA for d0a2a3a

• Added SourceLocation information to NonterminationDetection instrumentation for better error reporting

  ThomasHaas

  committed
  d61f89f

  Copy full SHA for d61f89f

• Added more complex liveness unit tests

  ThomasHaas

  committed
  8b275dd

  Copy full SHA for 8b275dd

• Increased Vulkan Liveness Test bounds to detect all non-termination

  ThomasHaas

  committed
  fc8e826

  Copy full SHA for fc8e826

• Merge branch 'refs/heads/development' into non-termination

  ThomasHaas

  committed
  e276384

  Copy full SHA for e276384

• Fix program_spec for Litmus tests to avoid considering non-terminating executions.

  ThomasHaas

  committed
  5d123b6

  Copy full SHA for 5d123b6

• Comment unsupported HSA tests

  hernanponcedeleon

  committed
  8e97c09

  Copy full SHA for 8e97c09

• Comment unsupported Obe tests

  hernanponcedeleon

  committed
  6c9eb1f

  Copy full SHA for 6c9eb1f

• Comment unsupported fair tests

  hernanponcedeleon

  committed
  9a467c1

  Copy full SHA for 9a467c1

Commits on Feb 17, 2025

• Refactor & clean-up

  ThomasHaas

  committed
  0b7e670

  Copy full SHA for 0b7e670

Commits on Feb 18, 2025

• Merge branch 'refs/heads/development' into non-termination

  Show description for d44ce40
  ThomasHaas

  committed
  d44ce40

  Copy full SHA for d44ce40