Repository navigation

spec for thread creation with pthread.h - #186

Open

simon-skylabs wants to merge 31 commits into

mainfrom

simon/thread-spec

Open

spec for thread creation with pthread.h#186
simon-skylabs wants to merge 31 commits into
mainfrom
simon/thread-spec

Commits on Oct 4, 2026
- define thread id type as wrapped integer
  Simon Hudon
  committed
  48e720e
- provide support for thread id as first class C++ values
  Simon Hudon
  committed
  e7a4130
- define process id
  Simon Hudon
  committed
  728d8c2
- re-export prelude definitions
  Simon Hudon
  committed
  ba0fdfc
- define weakly objective with respect to process id
  Simon Hudon
  committed
  9fca5f8
- skeleton for pthread.h specification
  Simon Hudon
  committed
  6a05103
Commits on Oct 5, 2026
- simple predicates and specs for pthread_attr_t
  Simon Hudon
  committed
  e29af87
- specify error codes
  Simon Hudon
  committed
  3d99af6
- predicates for threads
  Simon Hudon
  committed
  426c9f0
- spec for pthread_create
  Simon Hudon
  committed
  a60a024
- spec for pthread_join
  Simon Hudon
  committed
  859baf3
- spec for pthread_cancel and pthread_testcancel
  Simon Hudon
  committed
  a6860da
- spec for pthread ctor and dtor
  Simon Hudon
  committed
  7a365b8
- hints to find a function pointer's specification
  Simon Hudon
  committed
  bbf3a09
- test case for pthread specs
  Simon Hudon
  committed
  4dd89f0
- proof of the pthread test case
  Simon Hudon
  committed
  1014f2a
- revert Module Export
  Simon Hudon
  committed
  f479c07
- remove pthread cancelation specs
  Simon Hudon
  committed
  9f626f9
- remove cancelation-related predicates
  Simon Hudon
  committed
  9e6af0a
- remove testing of thread cancelation
  Simon Hudon
  committed
  666b89d
- inline comment in test
  Simon Hudon
  committed
  e69222c
- remove thread cancelation in test proofs
  Simon Hudon
  committed
  2755e24
- remove support for `pthread_attr_t`
  Simon Hudon
  committed
  e3da4ae
- remove `pthread_attr_t` from test case
  Simon Hudon
  committed
  8915086
- replace WeaklyObjective with Objective
  Simon Hudon
  committed
  0712d95
Commits on Oct 7, 2026
- move test case to test directory
  Simon Hudon
  committed
  ec13711
- pthread test: use existing cassert specs
  Simon Hudon
  committed
  9c10518
- fix dune.inc
  Simon Hudon
  committed
  b7656cf
- upstreamed some Objective lemmas
  Simon Hudon
  committed
  1040213
- remove dead code
  Simon Hudon
  committed
  17373e4
- fix spacing
  Simon Hudon
  committed
  c3dc661

Commits

Commits on Oct 4, 2026

Commits on Oct 5, 2026

Commits on Oct 7, 2026