Library mcertikos.proc.ThreadGenLinkSource
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatClightSem.
Require Import LAsmModuleSemDef.
Require Import CompCertiKOS.
Require Import GlobIdent.
Require Import CDataTypes.
Require Import ThreadGenAsmSource.
Definition PThread_impl: res LAsm.module :=
Require Import liblayers.compat.CompatClightSem.
Require Import LAsmModuleSemDef.
Require Import CompCertiKOS.
Require Import GlobIdent.
Require Import CDataTypes.
Require Import ThreadGenAsmSource.
Definition PThread_impl: res LAsm.module :=
watch out parentheses here:
ret (
(
(
group primitives according to the global variables that they use
((thread_yield ↦ threadyield_function) ⊕ (thread_sleep ↦ threadsleep_function) ⊕ (thread_kill ↦ threadkill_function))
) ⊕ ∅
) ⊕ ∅
for L64 and other passthrough primitives
).