Code

[DRAFT] Add interrupt handling#878

Code

Open

ThomasHaas wants to merge 39 commits intodevelopmenthernanponcedeleon/Dat3M:developmentfrom

interrupt_newhernanponcedeleon/Dat3M:interrupt_newCopy head branch name to clipboard

Commits

Commits on Sep 29, 2023

• Initial commit

  Show description for 3e38acf
  hernan-poncedeleon

  committed
  3e38acf

  Copy full SHA for 3e38acf

• Some tests

  Show description for 3ff12e7
  hernan-poncedeleon

  committed
  3ff12e7

  Copy full SHA for 3ff12e7

• Use fences instead of GenericVisibleEvent

  Show description for a1b4054
  hernan-poncedeleon

  committed
  a1b4054

  Copy full SHA for a1b4054

• Tag thread create and start events

  Show description for d2a0b71
  hernan-poncedeleon

  committed
  d2a0b71

  Copy full SHA for d2a0b71

• Add test cases

  Show description for 779cd35
  hernan-poncedeleon

  committed
  779cd35

  Copy full SHA for 779cd35

• Add harmless racy access annotation

  Show description for e3db364
  hernan-poncedeleon

  committed
  e3db364

  Copy full SHA for e3db364

Commits on Mar 21, 2025

• Merge branch 'refs/heads/development' into mergeBranch

  Show description for 4b48618
  ThomasHaas

  committed
  4b48618

  Copy full SHA for 4b48618

• added interrupts models and fixed tests

  ThomasHaas

  committed
  d7a97e2

  Copy full SHA for d7a97e2

Commits on Mar 25, 2025

• Changed assert to __VERIFIER_assert in vmm interrupts test (not yet in LKMM tests).

  ThomasHaas

  committed
  aac60ec

  Copy full SHA for aac60ec

Commits on Mar 26, 2025

• Updated remaining interrupt tests (mainly LKMM) to use __VERIFIER_assert

  ThomasHaas

  committed
  35f58f7

  Copy full SHA for 35f58f7

• Added new interrupts cat models that use explicit interrupt points (WIP)

  ThomasHaas

  committed
  c63350e

  Copy full SHA for c63350e

Commits on Mar 31, 2025

• Added CallEvent interface

  ThomasHaas

  committed
  e90aeb5

  Copy full SHA for e90aeb5

Commits on Apr 1, 2025

• - Added DynamicThreadCreate (pthread_create compiles to this one)

  Show description for 47c48ce
  ThomasHaas

  committed
  47c48ce

  Copy full SHA for 47c48ce

• Added DynamicThreadJoin (pthread_join compiles to this).

  Show description for 744fb33
  ThomasHaas

  committed
  744fb33

  Copy full SHA for 744fb33

• Added UniqueIdGenerator to generalize Function.dummyCount.

  Show description for ed794a1
  ThomasHaas

  committed
  ed794a1

  Copy full SHA for ed794a1

• Added ThreadReturn event (pthread_exit and top-level returns compiled to this).

  Show description for f4156a0
  ThomasHaas

  committed
  f4156a0

  Copy full SHA for f4156a0

• - Fixed encoding of AggregateType and ArrayType variables

  Show description for 8583041
  ThomasHaas

  committed
  8583041

  Copy full SHA for 8583041

Commits on Apr 2, 2025

• Cleanup

  ThomasHaas

  committed
  abd149b

  Copy full SHA for abd149b

• Fixed errors

  ThomasHaas

  committed
  5e74cfc

  Copy full SHA for 5e74cfc

• Fix error in NaiveDevirtualisation

  ThomasHaas

  committed
  2cb7c87

  Copy full SHA for 2cb7c87

Commits on Apr 3, 2025

• Merge branch 'refs/heads/better_threading' into interrupt_wip

  ThomasHaas

  committed
  4020b3e

  Copy full SHA for 4020b3e

• Added Thread.Type

  ThomasHaas

  committed
  5167df7

  Copy full SHA for 5167df7

• Connect IH control-flow to IT control-flow.

  Show description for 54c17ca
  ThomasHaas

  committed
  54c17ca

  Copy full SHA for 54c17ca

• Update interrupts-defs.cat to handle nested IHs

  ThomasHaas

  committed
  b87e32d

  Copy full SHA for b87e32d

• Add new Termination tests for interrupts

  ThomasHaas

  committed
  e071de3

  Copy full SHA for e071de3

• Add missing InterruptAnalysis class

  ThomasHaas

  committed
  0a3a912

  Copy full SHA for 0a3a912

Commits on Apr 9, 2025

• WIP: Visible non-termination events

  ThomasHaas

  committed
  bb167b3

  Copy full SHA for bb167b3

Commits on Apr 11, 2025

• WIP: Added new interrupt models that handle multiple IHs per thread

  ThomasHaas

  committed
  9f845a4

  Copy full SHA for 9f845a4

Commits on Apr 14, 2025

• Better interrupt models + new test benchmarks (no unit tests yet)

  ThomasHaas

  committed
  958aacc

  Copy full SHA for 958aacc

• Merge branch 'refs/heads/development' into merge

  Show description for f73edcf
  ThomasHaas

  committed
  f73edcf

  Copy full SHA for f73edcf

• Fixup after Merge

  ThomasHaas

  committed
  678a0b1

  Copy full SHA for 678a0b1

• Better handling of control flow of different IHs of the same thread

  ThomasHaas

  committed
  174096b

  Copy full SHA for 174096b

Commits on May 8, 2025

• Merge branch 'refs/heads/development' into merge

  Show description for 54b1617
  ThomasHaas

  committed
  54b1617

  Copy full SHA for 54b1617

• Fixup

  ThomasHaas

  committed
  2c297f4

  Copy full SHA for 2c297f4

• Remove outdated benchmarks

  ThomasHaas

  committed
  c6cfded

  Copy full SHA for c6cfded

• Remove Fence-tag from Nontermination marker

  ThomasHaas

  committed
  21a2799

  Copy full SHA for 21a2799

Commits on May 9, 2025

• Added comments about expected results of interrupt tests.

  ThomasHaas

  committed
  adb1907

  Copy full SHA for adb1907

Commits on May 14, 2025

• Merge branch 'refs/heads/development' into interrupt_new

  Show description for bcb60b4
  ThomasHaas

  committed
  bcb60b4

  Copy full SHA for bcb60b4

Commits on May 15, 2025

• Merge branch 'refs/heads/development' into interrupt_new

  ThomasHaas

  committed
  ae948c6

  Copy full SHA for ae948c6