[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base summary for Specification FLITPSCweak

FLITPSCGInv(0,0)disj-R3-ready(0,0)disj-W6-W7(0,0)disj-callPSCCOMPLETE-doReadPSC(0,0)disj-ctrIncPSC-globalPSCCRASH(0,0)disj-globalPSCCRASH-invFLITPSCWRITE(0,0)fliqtStep-lem(75,7)lstepf-W3(0,0)sel-ctrIncPSC-dottid(0,0)updsel--dotctr-dotmem(0,0)
FLITPSCInv(0,0)disj-R4-W1(0,0)disj-W6-crashed(0,0)disj-callPSCCOMPLETE-doWritePSC(0,0)disj-ctrIncPSC-globalPSCPERSISTuscFO(0,0)disj-globalPSCCRASH-pwbPSC(0,0)flitpscInit(0,0)lstepf-W4(0,0)sel-ctrReadPSC-dotl(0,0)updsel--dotctr-dotp(0,0)
FLITPSCLInv(0,0)disj-R4-W2(0,0)disj-W6-idle(0,0)disj-callPSCCOMPLETE-globalPSCCRASH(0,0)disj-ctrIncPSC-globalPSCPERSISTuscW(0,0)disj-globalPSCCRASH-retFLITPSCREAD(0,0)flitpscStep(0,0)lstepf-W5(0,0)sel-ctrReadPSC-dotn(0,0)updsel--dotctr-dotreaders(0,0)
FLITPSCRely(0,0)disj-R4-W3(0,0)disj-W6-ready(0,0)disj-callPSCCOMPLETE-globalPSCPERSISTuscFO(0,0)disj-ctrIncPSC-invFLITPSCREAD(0,0)disj-globalPSCCRASH-retFLITPSCWRITE(0,0)gen-FLITPSCAction(0,0)lstepf-W6(0,0)sel-ctrReadPSC-dottid(0,0)updsel--dotctr-dotwriters(0,0)
PSCCRASH(0,0)disj-R4-W4(0,0)disj-W7-crashed(0,0)disj-callPSCCOMPLETE-globalPSCPERSISTuscW(0,0)disj-ctrIncPSC-invFLITPSCWRITE(0,0)disj-globalPSCCRASH-sfencePSC(0,0)gen-FLITPSCGState(0,0)lstepf-W7(0,0)sel-doReadPSC-dotl(0,0)updsel--dotgstate-dotgstate(0,0)
PSCPERSIST_FO(0,0)disj-R4-W5(0,0)disj-W7-idle(0,0)disj-callPSCCOMPLETE-invFLITPSCREAD(0,0)disj-ctrIncPSC-pwbPSC(0,0)disj-globalPSCCRASH-tau(0,0)gen-FLITPSCLState(0,0)lstepf-idle-PSCRUN(0,0)sel-doReadPSC-dottid(0,0)updsel--dotgstate-dotlsf(0,0)
case-FLITPSCAction(0,0)disj-R4-W6(0,0)disj-W7-ready(0,0)disj-callPSCCOMPLETE-invFLITPSCWRITE(0,0)disj-ctrIncPSC-retFLITPSCREAD(0,0)disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW(0,0)gen-FLITPSCPC(0,0)lstepf-ready-FLITPSCREAD(0,0)sel-doReadPSC-dotv(0,0)updsel--dotgstate-dotpcf(0,0)
case-FLITPSCGState(0,0)disj-R4-W7(0,0)disj-atomicW1-atomicW5(0,0)disj-callPSCCOMPLETE-pwbPSC(0,0)disj-ctrIncPSC-retFLITPSCWRITE(0,0)disj-globalPSCPERSISTuscFO-invFLITPSCREAD(0,0)gen-FLITPSCState(0,0)lstepf-ready-FLITPSCWRITE(0,0)sel-doWritePSC-dotl(0,0)updsel--dotl-dotl(0,0)
case-FLITPSCLState(0,0)disj-R4-crashed(0,0)disj-atomicW1-callPSCCOMPLETE(0,0)disj-callPSCCOMPLETE-retFLITPSCREAD(0,0)disj-ctrIncPSC-sfencePSC(0,0)disj-globalPSCPERSISTuscFO-invFLITPSCWRITE(0,0)gstepf-R1(0,0)lstepf-ready-PSCCOMPLETE(0,0)sel-doWritePSC-dottid(0,0)updsel--dotl-dott(0,0)
case-FLITPSCPC(0,0)disj-R4-idle(0,0)disj-atomicW1-callPSCRUN(0,0)disj-callPSCCOMPLETE-retFLITPSCWRITE(0,0)disj-ctrIncPSC-tau(0,0)disj-globalPSCPERSISTuscFO-pwbPSC(0,0)gstepf-R2(0,0)not-pre-global-crash(2,1)sel-doWritePSC-dotv(0,0)updsel--dotl-dotv(0,0)
case-FLITPSCState(0,0)disj-R4-ready(0,0)disj-atomicW1-ctrDecPSC(0,0)disj-callPSCCOMPLETE-sfencePSC(0,0)disj-ctrReadPSC-doReadPSC(0,0)disj-globalPSCPERSISTuscFO-retFLITPSCREAD(0,0)gstepf-R3(0,0)not-pre-global-persist(2,1)sel-globalPSCPERSISTuscFO-dotinvPSCPERSISTuscFOl(0,0)updsel--dotlsf-dotgstate(0,0)
disj-R1-R2(0,0)disj-W1-W2(0,0)disj-atomicW1-ctrIncPSC(0,0)disj-callPSCCOMPLETE-tau(0,0)disj-ctrReadPSC-doWritePSC(0,0)disj-globalPSCPERSISTuscFO-retFLITPSCWRITE(0,0)gstepf-R4(0,0)not-pre-global-tsync(2,1)sel-globalPSCPERSISTuscW-dotinvPSCPERSISTuscWl(0,0)updsel--dotlsf-dotlsf(0,0)
disj-R1-R3(0,0)disj-W1-W3(0,0)disj-atomicW1-ctrReadPSC(0,0)disj-callPSCRUN-ctrDecPSC(0,0)disj-ctrReadPSC-globalPSCCRASH(0,0)disj-globalPSCPERSISTuscFO-sfencePSC(0,0)gstepf-W1(0,0)pcstepf-R1(0,0)sel-invFLITPSCREAD-dotinvFLITPSCREADl(0,0)updsel--dotlsf-dotpcf(0,0)
disj-R1-R4(0,0)disj-W1-W4(0,0)disj-atomicW1-doReadPSC(0,0)disj-callPSCRUN-ctrIncPSC(0,0)disj-ctrReadPSC-globalPSCPERSISTuscFO(0,0)disj-globalPSCPERSISTuscFO-tau(0,0)gstepf-W2(0,0)pcstepf-R2(0,0)sel-invFLITPSCREAD-dott(0,0)updsel--dotmem-dotctr(0,0)
disj-R1-W1(0,0)disj-W1-W5(0,0)disj-atomicW1-doWritePSC(0,0)disj-callPSCRUN-ctrReadPSC(0,0)disj-ctrReadPSC-globalPSCPERSISTuscW(0,0)disj-globalPSCPERSISTuscW-invFLITPSCREAD(0,0)gstepf-W3(0,0)pcstepf-R3(0,0)sel-invFLITPSCWRITE-dotinvFLITPSCWRITEl(0,0)updsel--dotmem-dotmem(0,0)
disj-R1-W2(0,0)disj-W1-W6(0,0)disj-atomicW1-globalPSCCRASH(0,0)disj-callPSCRUN-doReadPSC(0,0)disj-ctrReadPSC-invFLITPSCREAD(0,0)disj-globalPSCPERSISTuscW-invFLITPSCWRITE(0,0)gstepf-W4(0,0)pcstepf-R4(0,0)sel-invFLITPSCWRITE-dotinvFLITPSCWRITEv(0,0)updsel--dotmem-dotp(0,0)
disj-R1-W3(0,0)disj-W1-W7(0,0)disj-atomicW1-globalPSCPERSISTuscFO(0,0)disj-callPSCRUN-doWritePSC(0,0)disj-ctrReadPSC-invFLITPSCWRITE(0,0)disj-globalPSCPERSISTuscW-pwbPSC(0,0)gstepf-W5(0,0)pcstepf-W1(0,0)sel-invFLITPSCWRITE-dott(0,0)updsel--dotmem-dotreaders(0,0)
disj-R1-W4(0,0)disj-W1-crashed(0,0)disj-atomicW1-globalPSCPERSISTuscW(0,0)disj-callPSCRUN-globalPSCCRASH(0,0)disj-ctrReadPSC-pwbPSC(0,0)disj-globalPSCPERSISTuscW-retFLITPSCREAD(0,0)gstepf-W6(0,0)pcstepf-W2(0,0)sel-mkFLITPSCgs-dotctr(0,0)updsel--dotmem-dotwriters(0,0)
disj-R1-W5(0,0)disj-W1-idle(0,0)disj-atomicW1-invFLITPSCREAD(0,0)disj-callPSCRUN-globalPSCPERSISTuscFO(0,0)disj-ctrReadPSC-retFLITPSCREAD(0,0)disj-globalPSCPERSISTuscW-retFLITPSCWRITE(0,0)gstepf-W7(0,0)pcstepf-W3(0,0)sel-mkFLITPSCgs-dotmem(0,0)updsel--dotp-dotctr(0,0)
disj-R1-W6(0,0)disj-W1-ready(0,0)disj-atomicW1-invFLITPSCWRITE(0,0)disj-callPSCRUN-globalPSCPERSISTuscW(0,0)disj-ctrReadPSC-retFLITPSCWRITE(0,0)disj-globalPSCPERSISTuscW-sfencePSC(0,0)gstepf-idle-PSCRUN(0,0)pcstepf-W4(0,0)sel-mkFLITPSCgs-dotp(0,0)updsel--dotp-dotmem(0,0)
disj-R1-W7(0,0)disj-W2-W3(0,0)disj-atomicW1-pwbPSC(0,0)disj-callPSCRUN-invFLITPSCREAD(0,0)disj-ctrReadPSC-sfencePSC(0,0)disj-globalPSCPERSISTuscW-tau(0,0)gstepf-ready(0,0)pcstepf-W5(0,0)sel-mkFLITPSCgs-dotreaders(0,0)updsel--dotp-dotp(0,0)
disj-R1-crashed(0,0)disj-W2-W4(0,0)disj-atomicW1-retFLITPSCREAD(0,0)disj-callPSCRUN-invFLITPSCWRITE(0,0)disj-ctrReadPSC-tau(0,0)disj-idle-ready(0,0)inj-callPSCCOMPLETE(0,0)pcstepf-W6(0,0)sel-mkFLITPSCgs-dotwriters(0,0)updsel--dotp-dotreaders(0,0)
disj-R1-idle(0,0)disj-W2-W5(0,0)disj-atomicW1-retFLITPSCWRITE(0,0)disj-callPSCRUN-pwbPSC(0,0)disj-doReadPSC-doWritePSC(0,0)disj-invFLITPSCREAD-invFLITPSCWRITE(0,0)inj-callPSCRUN(0,0)pcstepf-W7(0,0)sel-mkFLITPSCls-dotl(0,0)updsel--dotp-dotwriters(0,0)
disj-R1-ready(0,0)disj-W2-W6(0,0)disj-atomicW1-sfencePSC(0,0)disj-callPSCRUN-retFLITPSCREAD(0,0)disj-doReadPSC-globalPSCCRASH(0,0)disj-invFLITPSCREAD-pwbPSC(0,0)inj-ctrDecPSC(0,0)pcstepf-idle-PSCRUN(0,0)sel-mkFLITPSCls-dott(0,0)updsel--dotpcf-dotgstate(0,0)
disj-R2-R3(0,0)disj-W2-W7(0,0)disj-atomicW1-tau(0,0)disj-callPSCRUN-retFLITPSCWRITE(0,0)disj-doReadPSC-globalPSCPERSISTuscFO(0,0)disj-invFLITPSCREAD-retFLITPSCREAD(0,0)inj-ctrIncPSC(0,0)pcstepf-ready-FLITPSCREAD(0,0)sel-mkFLITPSCls-dotv(0,0)updsel--dotpcf-dotlsf(0,0)
disj-R2-R4(0,0)disj-W2-crashed(0,0)disj-atomicW5-callPSCCOMPLETE(0,0)disj-callPSCRUN-sfencePSC(0,0)disj-doReadPSC-globalPSCPERSISTuscW(0,0)disj-invFLITPSCREAD-retFLITPSCWRITE(0,0)inj-ctrReadPSC(0,0)pcstepf-ready-FLITPSCWRITE(0,0)sel-mkstate-dotgstate(0,0)updsel--dotpcf-dotpcf(0,0)
disj-R2-W1(0,0)disj-W2-idle(0,0)disj-atomicW5-callPSCRUN(0,0)disj-callPSCRUN-tau(0,0)disj-doReadPSC-invFLITPSCREAD(0,0)disj-invFLITPSCREAD-sfencePSC(0,0)inj-doReadPSC(0,0)pcstepf-ready-PSCCOMPLETE(0,0)sel-mkstate-dotlsf(0,0)updsel--dotreaders-dotctr(0,0)
disj-R2-W2(0,0)disj-W2-ready(0,0)disj-atomicW5-ctrDecPSC(0,0)disj-crashed-idle(0,0)disj-doReadPSC-invFLITPSCWRITE(0,0)disj-invFLITPSCREAD-tau(0,0)inj-doWritePSC(0,0)pre-R1(0,0)sel-mkstate-dotpcf(0,0)updsel--dotreaders-dotmem(0,0)
disj-R2-W3(0,0)disj-W3-W4(0,0)disj-atomicW5-ctrIncPSC(0,0)disj-crashed-ready(0,0)disj-doReadPSC-pwbPSC(0,0)disj-invFLITPSCWRITE-pwbPSC(0,0)inj-globalPSCPERSISTuscFO(0,0)pre-R2(0,0)sel-pwbPSC-dotl(0,0)updsel--dotreaders-dotp(0,0)
disj-R2-W4(0,0)disj-W3-W5(0,0)disj-atomicW5-ctrReadPSC(0,0)disj-ctrDecPSC-ctrIncPSC(0,0)disj-doReadPSC-retFLITPSCREAD(0,0)disj-invFLITPSCWRITE-retFLITPSCREAD(0,0)inj-globalPSCPERSISTuscW(0,0)pre-R3(0,0)sel-pwbPSC-dottid(0,0)updsel--dotreaders-dotreaders(0,0)
disj-R2-W5(0,0)disj-W3-W6(0,0)disj-atomicW5-doReadPSC(0,0)disj-ctrDecPSC-ctrReadPSC(0,0)disj-doReadPSC-retFLITPSCWRITE(0,0)disj-invFLITPSCWRITE-retFLITPSCWRITE(0,0)inj-invFLITPSCREAD(0,0)pre-R4(0,0)sel-retFLITPSCREAD-dotretFLITPSCREADv(0,0)updsel--dotreaders-dotwriters(0,0)
disj-R2-W6(0,0)disj-W3-W7(0,0)disj-atomicW5-doWritePSC(0,0)disj-ctrDecPSC-doReadPSC(0,0)disj-doReadPSC-sfencePSC(0,0)disj-invFLITPSCWRITE-sfencePSC(0,0)inj-invFLITPSCWRITE(0,0)pre-W1(0,0)sel-retFLITPSCREAD-dott(0,0)updsel--dott-dotl(0,0)
disj-R2-W7(0,0)disj-W3-crashed(0,0)disj-atomicW5-globalPSCCRASH(0,0)disj-ctrDecPSC-doWritePSC(0,0)disj-doReadPSC-tau(0,0)disj-invFLITPSCWRITE-tau(0,0)inj-mkFLITPSCgs(0,0)pre-W2(0,0)sel-retFLITPSCWRITE-dott(0,0)updsel--dott-dott(0,0)
disj-R2-crashed(0,0)disj-W3-idle(0,0)disj-atomicW5-globalPSCPERSISTuscFO(0,0)disj-ctrDecPSC-globalPSCCRASH(0,0)disj-doWritePSC-globalPSCCRASH(0,0)disj-pwbPSC-retFLITPSCREAD(0,0)inj-mkFLITPSCls(0,0)pre-W3(0,0)sel-sfencePSC-dottid(0,0)updsel--dott-dotv(0,0)
disj-R2-idle(0,0)disj-W3-ready(0,0)disj-atomicW5-globalPSCPERSISTuscW(0,0)disj-ctrDecPSC-globalPSCPERSISTuscFO(0,0)disj-doWritePSC-globalPSCPERSISTuscFO(0,0)disj-pwbPSC-retFLITPSCWRITE(0,0)inj-mkstate(0,0)pre-W4(0,0)upd-mkFLITPSCgs-dotctr(0,0)updsel--dotv-dotl(0,0)
disj-R2-ready(0,0)disj-W4-W5(0,0)disj-atomicW5-invFLITPSCREAD(0,0)disj-ctrDecPSC-globalPSCPERSISTuscW(0,0)disj-doWritePSC-globalPSCPERSISTuscW(0,0)disj-pwbPSC-sfencePSC(0,0)inj-pwbPSC(0,0)pre-W5(0,0)upd-mkFLITPSCgs-dotmem(0,0)updsel--dotv-dott(0,0)
disj-R3-R4(0,0)disj-W4-W6(0,0)disj-atomicW5-invFLITPSCWRITE(0,0)disj-ctrDecPSC-invFLITPSCREAD(0,0)disj-doWritePSC-invFLITPSCREAD(0,0)disj-pwbPSC-tau(0,0)inj-retFLITPSCREAD(0,0)pre-W6(0,0)upd-mkFLITPSCgs-dotp(0,0)updsel--dotv-dotv(0,0)
disj-R3-W1(0,0)disj-W4-W7(0,0)disj-atomicW5-pwbPSC(0,0)disj-ctrDecPSC-invFLITPSCWRITE(0,0)disj-doWritePSC-invFLITPSCWRITE(0,0)disj-retFLITPSCREAD-retFLITPSCWRITE(0,0)inj-retFLITPSCWRITE(0,0)pre-W7(0,0)upd-mkFLITPSCgs-dotreaders(0,0)updsel--dotwriters-dotctr(0,0)
disj-R3-W2(0,0)disj-W4-crashed(0,0)disj-atomicW5-retFLITPSCREAD(0,0)disj-ctrDecPSC-pwbPSC(0,0)disj-doWritePSC-pwbPSC(0,0)disj-retFLITPSCREAD-sfencePSC(0,0)inj-sfencePSC(0,0)pre-crashed(0,0)upd-mkFLITPSCgs-dotwriters(0,0)updsel--dotwriters-dotmem(0,0)
disj-R3-W3(0,0)disj-W4-idle(0,0)disj-atomicW5-retFLITPSCWRITE(0,0)disj-ctrDecPSC-retFLITPSCREAD(0,0)disj-doWritePSC-retFLITPSCREAD(0,0)disj-retFLITPSCREAD-tau(0,0)lstep(0,0)pre-idle(0,0)upd-mkFLITPSCls-dotl(0,0)updsel--dotwriters-dotp(0,0)
disj-R3-W4(0,0)disj-W4-ready(0,0)disj-atomicW5-sfencePSC(0,0)disj-ctrDecPSC-retFLITPSCWRITE(0,0)disj-doWritePSC-retFLITPSCWRITE(0,0)disj-retFLITPSCWRITE-sfencePSC(0,0)lstepf-R1(0,0)pre-ready(0,0)upd-mkFLITPSCls-dott(0,0)updsel--dotwriters-dotreaders(0,0)
disj-R3-W5(0,0)disj-W5-W6(0,0)disj-atomicW5-tau(0,0)disj-ctrDecPSC-sfencePSC(0,0)disj-doWritePSC-sfencePSC(0,0)disj-retFLITPSCWRITE-tau(0,0)lstepf-R2(0,0)sel-callPSCCOMPLETE-dott(0,0)upd-mkFLITPSCls-dotv(0,0)updsel--dotwriters-dotwriters(0,0)
disj-R3-W6(0,0)disj-W5-W7(0,0)disj-callPSCCOMPLETE-callPSCRUN(0,0)disj-ctrDecPSC-tau(0,0)disj-doWritePSC-tau(0,0)disj-sfencePSC-tau(0,0)lstepf-R3(0,0)sel-callPSCRUN-dott(0,0)upd-mkstate-dotgstate(0,0)
disj-R3-W7(0,0)disj-W5-crashed(0,0)disj-callPSCCOMPLETE-ctrDecPSC(0,0)disj-ctrIncPSC-ctrReadPSC(0,0)disj-globalPSCCRASH-globalPSCPERSISTuscFO(0,0)elim-mkFLITPSCgs(0,0)lstepf-R4(0,0)sel-ctrDecPSC-dotl(0,0)upd-mkstate-dotlsf(0,0)
disj-R3-crashed(0,0)disj-W5-idle(0,0)disj-callPSCCOMPLETE-ctrIncPSC(0,0)disj-ctrIncPSC-doReadPSC(0,0)disj-globalPSCCRASH-globalPSCPERSISTuscW(0,0)elim-mkFLITPSCls(0,0)lstepf-W1(0,0)sel-ctrDecPSC-dottid(0,0)upd-mkstate-dotpcf(0,0)
disj-R3-idle(0,0)disj-W5-ready(0,0)disj-callPSCCOMPLETE-ctrReadPSC(0,0)disj-ctrIncPSC-doWritePSC(0,0)disj-globalPSCCRASH-invFLITPSCREAD(0,0)elim-mkstate(0,0)lstepf-W2(0,0)sel-ctrIncPSC-dotl(0,0)updsel--dotctr-dotctr(0,0)