Code

Experimental concurrency support#730

Code

Merged

abakst merged 30 commits intomasterGaloisInc/crucible:masterfrom concurrencyGaloisInc/crucible:concurrencyCopy head branch name to clipboardMay 13, 2021

+8,943-150

Commits

Commits on May 4, 2021

• fix for crucibles work

  abakst

  committed
  967dd8f

  Copy full SHA for 967dd8f

• Add parser that returns global variables

  abakst

  committed
  e4ea8c3

  Copy full SHA for e4ea8c3

• Display an error if crucible-syntax finds no blocks in a function.

  abakst

  committed
  782fefd

  Copy full SHA for 782fefd

• Make Nats showable in crucible-syntax

  abakst

  committed
  8755b82

  Copy full SHA for 8755b82

• Add crucible-concurrency, an library enabling support

  Show description for 420d3a4
  abakst

  committed
  420d3a4

  Copy full SHA for 420d3a4

• Add tests and examples for crucible-concurrency

  abakst

  committed
  8eaa249

  Copy full SHA for 8eaa249

• Add core primitives to support concurrency in crux-mir libraries.

  abakst

  committed
  8ab2dfe

  Copy full SHA for 8ab2dfe

• Model rust library concurrency functions using primitives from

  Show description for b38fdfb
  abakst

  committed
  b38fdfb

  Copy full SHA for b38fdfb

• Add experimental concurrency support to crux-mir, using crucible-concurrency.

  abakst

  committed
  94c467d

  Copy full SHA for 94c467d

• Add some concurrency testcases.

  abakst

  committed
  87fb85b

  Copy full SHA for 87fb85b

• Add notes on the experimental concurrency support in crux-mir.

  abakst

  committed
  647fb20

  Copy full SHA for 647fb20

• Loosen constraints on base.

  abakst

  committed
  50abdba

  Copy full SHA for 50abdba

Commits on May 5, 2021

• Fix comment typo in concurrency.rs

  Show description for 5184d6e
  

  abakst

  and

  RyanGlScott

  authored
  5184d6e

  Copy full SHA for 5184d6e

• Remove erroneously committed file.

  abakst

  committed
  fa316f7

  Copy full SHA for fa316f7

• Rename package to crucible-concurrency, and indicate that "Crucibles"

  Show description for 12227ca
  abakst

  committed
  12227ca

  Copy full SHA for 12227ca

• Remove unused Handle to /dev/null in test/Main.hs. (It was used before switching to Crux.)

  abakst

  committed
  868b8e6

  Copy full SHA for 868b8e6

• Remove incomplete tests

  abakst

  committed
  1964065

  Copy full SHA for 1964065

Commits on May 6, 2021

• Remove redundant module (CruciblesMain was moved to CrucesMain)

  abakst

  committed
  23c8026

  Copy full SHA for 23c8026

• Expose ppSchedExecutionsDPOR in Crucibles.DPOR.

  abakst

  committed
  c660657

  Copy full SHA for c660657

• Remove commented-out code

  abakst

  committed
  5724e85

  Copy full SHA for 5724e85

Commits on May 7, 2021

• Fix configuration of opaque atomics in liballoc and libstd.

  abakst

  committed
  c331372

  Copy full SHA for c331372

• Remove unnecessary [[ in favor of [

  abakst

  committed
  e970e42

  Copy full SHA for e970e42

• Remove stale comment

  abakst

  committed
  7d27aca

  Copy full SHA for 7d27aca

• Merge Index_RefPath names by not printing the index (which could be

  Show description for fad7717
  abakst

  committed
  fad7717

  Copy full SHA for fad7717

• Remove unsoundness in generating resource names from Index_RefPath.

  Show description for ec304a6
  abakst

  committed
  ec304a6

  Copy full SHA for ec304a6

• Change T to *const T in arguments to concurrency primitives.

  abakst

  committed
  07b5f57

  Copy full SHA for 07b5f57

• Add explanation for not handling MirReference_Integer in mirRefName.

  abakst

  committed
  e6551d4

  Copy full SHA for e6551d4

Commits on May 12, 2021

• Port many tests from svcomp. The tool struggles with some benchmarks due to the usual state explosion issues.

  abakst

  committed
  594dc0c

  Copy full SHA for 594dc0c

• Add pthread-finding-k-matches, which is a good example of our issues with branching.

  abakst

  committed
  96c57c7

  Copy full SHA for 96c57c7

• Relax instance size of finding-k-matches

  abakst

  committed
  b486e57

  Copy full SHA for b486e57