diff --git a/router/dataplane.go b/router/dataplane.go index 6ad2c3181..e00529858 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -98,7 +98,6 @@ import ( "github.com/scionproto/scion/router/control" // @ . "github.com/scionproto/scion/verification/utils/definitions" // @ fl "github.com/scionproto/scion/verification/utils/floats" - // @ gsync "github.com/scionproto/scion/verification/utils/ghost_sync" // @ sl "github.com/scionproto/scion/verification/utils/slices" // @ "github.com/scionproto/scion/verification/utils/seqs" // @ socketspec "golang.org/x/net/internal/socket/" @@ -149,11 +148,15 @@ type bfdSession interface { type BatchConn interface { // @ pred Mem() + // @ atomic // @ requires acc(Mem(), _) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() // @ requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) + // contracts for IO-spec + // @ requires Prophecy(prophecyM) + // @ requires io.token(place) && MultiReadBio(place, prophecyM) // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ (msgs[i].Mem() && msgs[i].HasActiveAddr()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) @@ -167,8 +170,6 @@ type BatchConn interface { // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ ensures err != nil ==> err.ErrorMem() // contracts for IO-spec - // @ requires Prophecy(prophecyM) - // @ requires io.token(place) && MultiReadBio(place, prophecyM) // @ ensures err != nil ==> prophecyM == 0 // @ ensures err == nil ==> prophecyM == n // @ ensures io.token(old(MultiReadBioNext(place, prophecyM))) @@ -183,6 +184,7 @@ type BatchConn interface { // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) + // @ atomic // @ requires acc(Mem(), _) // (VerifiedSCION) opted for less reusable spec for WriteBatch for // performance reasons. @@ -825,7 +827,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ reveal d.PreWellConfigured() // @ reveal d.DpAgreesWithSpec(dp) // @ ) - // @ ghost ioLockRun, ioSharedArgRun := InitSharedInv(dp, place, state) + // @ ghost ioSharedArgRun := InitSharedInv(dp, place, state) d.initMetrics( /*@ dp @*/ ) read /*@@@*/ := @@ -847,10 +849,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ requires dp.Valid() // @ requires let d := *dPtr in // @ d.DpAgreesWithSpec(dp) - // @ requires acc(ioLock.LockP(), _) - // @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> + // @ requires Invariant(SharedInv!) // @ #backend[moreJoins()] - func /*@ rc @*/ (ingressID uint16, rd BatchConn, dPtr **DataPlane /*@, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { + func /*@ rc @*/ (ingressID uint16, rd BatchConn, dPtr **DataPlane /*@, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { d := *dPtr msgs := conn.NewReadMessages(inputBatchCnt) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> @@ -926,14 +927,13 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant let ubuf := processor.sInitBufferUBuf() in // @ acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm) // @ invariant processor.getIngressID() == ingressID - // @ invariant acc(ioLock.LockP(), _) - // @ invariant ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> + // @ invariant Invariant(SharedInv!) // @ invariant d.DpAgreesWithSpec(dp) && dp.Valid() for d.running { // @ ghost ioIngressID := path.ifsToIO_ifs(ingressID) // Multi recv event - // @ ghost ioLock.Lock() - // @ unfold SharedInv!< dp, ioSharedArg !>() + // @ critical SharedInv! ( + // @ unfold SharedInv!() // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State // @ ghost numberOfReceivedPacketsProphecy := AllocProphecy() // @ ExtractMultiReadBio(dp, t, numberOfReceivedPacketsProphecy, s) @@ -958,7 +958,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ MsgToAbsVal(&msgs[i], ingressID) == old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)[i]) // @ MultiElemWitnessConv(ioSharedArg.IBufY, ioIngressID, ioValSeq) // @ fold SharedInv!< dp, ioSharedArg !>() - // @ ioLock.Unlock() + // @ ) // End of multi recv event // @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() @@ -1010,8 +1010,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant pkts <= len(ioValSeq) // @ invariant d.DpAgreesWithSpec(dp) && dp.Valid() // @ invariant ioIngressID == path.ifsToIO_ifs(ingressID) - // @ invariant acc(ioLock.LockP(), _) - // @ invariant ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> + // @ invariant Invariant(SharedInv!) // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] // @ invariant MultiElemWitnessWithIndex(ioSharedArg.IBufY, ioIngressID, ioValSeq, i0) @@ -1062,7 +1061,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ sl.SplitRange_Bytes(p.Buffers[0], 0, p.N, HalfPerm) // @ assert sl.Bytes(tmpBuf, 0, p.N) // @ assert sl.Bytes(tmpBuf, 0, len(tmpBuf)) - result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp @*/) + result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioSharedArg, dp @*/) // (VerifiedSCION) This assertion is crucial to keep verification stable. Without it, // the fold operation in the branch protected by the condition `result.OutConn == nil` // may fail non-deterministically. @@ -1142,7 +1141,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ assert result.OutPkt != nil ==> newAbsPkt == // @ absIO_val(writeMsgs[0].Buffers[0], result.EgressID) // @ fold acc(writeMsgs[0].Mem(), R50) - // @ ghost ioLock.Lock() + // @ critical SharedInv! ( // @ unfold SharedInv!< dp, ioSharedArg !>() // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State // @ ghost if(newAbsPkt.isValPkt) { @@ -1157,7 +1156,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta _, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT /*@, result.EgressID, t, newAbsPkt @*/) // @ ghost *ioSharedArg.Place = tN // @ fold SharedInv!< dp, ioSharedArg !>() - // @ ghost ioLock.Unlock() + // @ ) // @ unfold acc(writeMsgs[0].Mem(), R50) // @ ghost if addrAliasesPkt && result.OutAddr != nil { // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.Bytes(tmpBuf, 0, len(tmpBuf)), R15) @@ -1261,8 +1260,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant d.getMacFactory() != nil // @ invariant dp.Valid() // @ invariant d.DpAgreesWithSpec(dp) - // @ invariant acc(ioLockRun.LockP(), _) - // @ invariant ioLockRun.LockInv() == SharedInv!< dp, ioSharedArgRun !> + // @ invariant Invariant(SharedInv!) // @ decreases len(externals) - len(visited) for ifID, v := range externals /*@ with visited @*/ { cl := @@ -1278,18 +1276,17 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // contracts for IO-spec // @ requires dp.Valid() // @ requires d.DpAgreesWithSpec(dp) - // @ requires acc(ioLock.LockP(), _) - // @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> - func /*@ closure2 @*/ (i uint16, c BatchConn /*@, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { + // @ requires Invariant(SharedInv!) + func /*@ closure2 @*/ (i uint16, c BatchConn /*@, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { defer log.HandlePanic() - read(i, c, &d /*@, ioLock, ioSharedArg, dp @*/) //@ as rc + read(i, c, &d /*@, ioSharedArg, dp @*/) //@ as rc } // @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R50) } // @ assert v elem range(d.external) // @ assert acc(v.Mem(), _) // @ d.InDomainExternalInForwardingMetrics3(ifID) // @ ghost if d.external != nil { fold acc(accBatchConn(d.external), R50) } - go cl(ifID, v /*@, ioLockRun, ioSharedArgRun, dp @*/) //@ as closure2 + go cl(ifID, v /*@, ioSharedArgRun, dp @*/) //@ as closure2 } cl := // @ requires acc(&read, _) && read implements rc @@ -1303,14 +1300,13 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // contracts for IO-spec // @ requires dp.Valid() // @ requires d.DpAgreesWithSpec(dp) - // @ requires acc(ioLock.LockP(), _) - // @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> - func /*@ closure3 @*/ (c BatchConn /*@, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { + // @ requires Invariant(SharedInv!) + func /*@ closure3 @*/ (c BatchConn /*@, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) { defer log.HandlePanic() - read(0, c, &d /*@, ioLock, ioSharedArg, dp @*/) //@ as rc + read(0, c, &d /*@, ioSharedArg, dp @*/) //@ as rc } // @ d.getInternalMem() - go cl(d.internal /*@, ioLockRun, ioSharedArgRun, dp @*/) //@ as closure3 + go cl(d.internal /*@, ioSharedArgRun, dp @*/) //@ as closure3 d.mtx.Unlock() // @ assert acc(ctx.Mem(), _) @@ -1516,8 +1512,7 @@ func (p *scionPacketProcessor) reset() (err error) { // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires dp.Valid() -// @ requires acc(ioLock.LockP(), _) -// @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +// @ requires Invariant(SharedInv!) // @ requires let absPkt := absIO_val(rawPkt, p.getIngressID()) in // @ absPkt.isValPkt ==> ElemWitness(ioSharedArg.IBufY, path.ifsToIO_ifs(p.getIngressID()), absPkt.ValPkt_2) // @ ensures respr.OutPkt != nil ==> @@ -1529,7 +1524,7 @@ func (p *scionPacketProcessor) reset() (err error) { // @ decreases 0 if sync.IgnoreBlockingForTermination() // @ #backend[moreJoins(1)] func (p *scionPacketProcessor) processPkt(rawPkt []byte, - srcAddr *net.UDPAddr /*@, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { + srcAddr *net.UDPAddr /*@, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { if err := p.reset(); err != nil { // @ fold p.sInitD().validResult(processResult{}, false) @@ -1649,7 +1644,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm) // @ } // @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt)) - v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioSharedArg, dp @*/ ) // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/ @@ -1825,8 +1820,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ requires (typeOf(p.scionLayer.GetPath(ub)) == *scion.Raw) ==> // @ p.scionLayer.EqAbsHeader(ub) && p.scionLayer.ValidScionInitSpec(ub) // @ requires p.scionLayer.EqPathType(ub) -// @ requires acc(ioLock.LockP(), _) -// @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +// @ requires Invariant(SharedInv!) // @ requires let absPkt := absIO_val(p.rawPkt, p.ingressID) in // @ absPkt.isValPkt ==> ElemWitness(ioSharedArg.IBufY, path.ifsToIO_ifs(p.ingressID), absPkt.ValPkt_2) // @ ensures reserr == nil && newAbsPkt.isValPkt ==> @@ -1837,7 +1831,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ newAbsPkt.isValUnsupported // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.ValUnit{}) // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { +func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { var ok bool // @ unfold acc(p.scionLayer.Mem(ub), R20) @@ -1850,7 +1844,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // @ fold p.d.validResult(processResult{}, false) return processResult{}, malformedPath /*@ , false, io.ValUnit{} @*/ } - return p.process( /*@ ub, llIsNil, startLL, endLL , ioLock, ioSharedArg, dp @*/ ) + return p.process( /*@ ub, llIsNil, startLL, endLL, ioSharedArg, dp @*/ ) } // @ trusted @@ -3852,8 +3846,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ requires p.d.DpAgreesWithSpec(dp) // @ requires dp.Valid() // @ requires p.scionLayer.EqAbsHeader(ub) && p.scionLayer.EqPathType(ub) && p.scionLayer.ValidScionInitSpec(ub) -// @ requires acc(ioLock.LockP(), _) -// @ requires ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +// @ requires Invariant(SharedInv!) // @ requires let absPkt := absIO_val(ub, p.ingressID) in // @ absPkt.isValPkt ==> ElemWitness(ioSharedArg.IBufY, path.ifsToIO_ifs(p.ingressID), absPkt.ValPkt_2) // @ ensures reserr == nil && newAbsPkt.isValPkt ==> @@ -3870,7 +3863,6 @@ func (p *scionPacketProcessor) process( // @ ghost llIsNil bool, // @ ghost startLL int, // @ ghost endLL int, -// @ ghost ioLock gpointer[gsync.GhostMutex], // @ ghost ioSharedArg SharedArg, // @ ghost dp io.DataPlaneSpec, ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) { @@ -3946,7 +3938,7 @@ func (p *scionPacketProcessor) process( // @ fold p.d.validResult(processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, aliasesUb) // @ assert ub === p.rawPkt // @ ghost if(slayers.IsSupportedPkt(ub)) { - // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioLock, ioSharedArg, dp) + // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioSharedArg, dp) // @ } // @ newAbsPkt = reveal absIO_val(p.rawPkt, 0) return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@, aliasesUb, newAbsPkt @*/ @@ -4017,9 +4009,9 @@ func (p *scionPacketProcessor) process( // @ nextPkt = absPkt(ub) // @ ghost if(slayers.IsSupportedPkt(ub)) { // @ ghost if(!p.segmentChange) { - // @ ExternalEnterOrExitEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioLock, ioSharedArg, dp) + // @ ExternalEnterOrExitEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioSharedArg, dp) // @ } else { - // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioLock, ioSharedArg, dp) + // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioSharedArg, dp) // @ } // @ } // @ newAbsPkt = reveal absIO_val(p.rawPkt, egressID) @@ -4035,9 +4027,9 @@ func (p *scionPacketProcessor) process( // @ p.d.getInternal() // @ ghost if(slayers.IsSupportedPkt(ub)) { // @ if(!p.segmentChange) { - // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioLock, ioSharedArg, dp) + // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioSharedArg, dp) // @ } else { - // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioLock, ioSharedArg, dp) + // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.Ifs], ioSharedArg, dp) // @ } // @ } // @ newAbsPkt = reveal absIO_val(p.rawPkt, 0) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 1b8207c17..33851a190 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -17,7 +17,6 @@ package router import ( - gsync "verification/utils/ghost_sync" "verification/utils/resalgebra" io "verification/io" ) @@ -38,21 +37,20 @@ pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) { // initialize the shared invariant: ghost requires io.token(p) && dp.dp3s_iospec_ordered(s, p) -ensures m.LockP() && m.LockInv() == SharedInv!< dp, y !> +ensures Invariant(SharedInv!) decreases func InitSharedInv( dp io.DataPlaneSpec, p io.Place, - s io.Dp3sStateLocal) (m gpointer[gsync.GhostMutex], y SharedArg) { - mV@ := gsync.GhostMutex{} - m = &mV + s io.Dp3sStateLocal) (y SharedArg) { pE@ := p sE@ := s yI := InitElemAuth(s.ibuf) yO := InitElemAuth(s.obuf) y := SharedArg{&pE, &sE, yI, yO} - fold SharedInv!< dp, y !>() - m.SetInv(SharedInv!< dp, y !>) + fold SharedInv!() + EstablishInvariant(SharedInv!) + return y } /////////////////////////////////////// Prophecies /////////////////////////////////////// diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 859c31674..1fa730db3 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -22,7 +22,6 @@ import ( "github.com/scionproto/scion/pkg/slayers" . "verification/utils/definitions" io "verification/io" - gsync "verification/utils/ghost_sync" sl "verification/utils/slices" ) @@ -153,6 +152,7 @@ pure func AbsVerifyCurrentMACConstraint(pkt io.Pkt, dp io.DataPlaneSpec) bool { // from a different AS (ingressID != none[io.Ifs]) // and will be forwarded to another border router within the AS (egressID == none[io.Ifs]) ghost +opensInvariants requires dp.Valid() requires ingressID != none[io.Ifs] requires egressID == none[io.Ifs] @@ -162,18 +162,17 @@ requires newPkt == AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID) requires AbsValidateIngressIDConstraint(oldPkt, ingressID) requires AbsVerifyCurrentMACConstraint(newPkt, dp) requires len(newPkt.CurrSeg.Future) == 1 || AbsValidateEgressIDConstraint(newPkt, true, dp) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) decreases -func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { +func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID) reveal AbsValidateIngressIDConstraint(oldPkt, ingressID) reveal AbsVerifyCurrentMACConstraint(newPkt, dp) if(len(newPkt.CurrSeg.Future) != 1) { reveal AbsValidateEgressIDConstraint(newPkt, true, dp) } - AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) + AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp) } // Either this executes the IO enter event whenever a pkt was received @@ -183,6 +182,7 @@ func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, // within the AS (ingressID == none[io.Ifs]) // and will leave the AS (egressID != none[io.Ifs]) ghost +opensInvariants requires dp.Valid() requires egressID != none[io.Ifs] requires get(egressID) elem domain(dp.GetNeighborIAs()) @@ -193,11 +193,10 @@ requires AbsVerifyCurrentMACConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, requires AbsValidateEgressIDConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID), (ingressID != none[io.Ifs]), dp) requires AbsEgressInterfaceConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID), egressID) requires newPkt == AbsProcessEgress(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) decreases -func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { +func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { reveal dp.Valid() nextPkt := reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID) reveal AbsValidateIngressIDConstraint(oldPkt, ingressID) @@ -206,9 +205,9 @@ func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io reveal AbsValidateEgressIDConstraint(nextPkt, (ingressID != none[io.Ifs]), dp) reveal AbsProcessEgress(nextPkt) if(ingressID == none[io.Ifs]){ - AtomicExit(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) + AtomicExit(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp) } else { - AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) + AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp) } } @@ -216,6 +215,7 @@ func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io // from a different AS (ingressID != none[io.Ifs]) // and a segment switch was performed. ghost +opensInvariants requires dp.Valid() requires ingressID != none[io.Ifs] requires oldPkt.PathNotFullyTraversed() @@ -234,11 +234,10 @@ requires egressID == none[io.Ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)) requires egressID != none[io.Ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) decreases -func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { +func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { reveal dp.Valid() intermediatePkt1 := reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID) intermediatePkt2 := reveal AbsDoXover(intermediatePkt1) @@ -250,5 +249,5 @@ func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID) reveal AbsProcessEgress(intermediatePkt2) } - AtomicXover(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) + AtomicXover(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp) } diff --git a/router/io-spec-atomic-events.gobra b/router/io-spec-atomic-events.gobra index 13f0a781c..a4b4a095a 100644 --- a/router/io-spec-atomic-events.gobra +++ b/router/io-spec-atomic-events.gobra @@ -15,21 +15,17 @@ // +gobra // This file contains the definition of operations that perform the atomic transitions of state -// in the IO spec. They all take a gpointer[gsync.GhostMutex], which acts as a logical invariant, because Gobra -// does not support invariants natively. As such, we can only get access to the invariants if we -// first lock the mutex. Even though all these operations are -// terminating, Gobra cannot currently prove this and thus, we assume termination for all methods -// in this file. +// in the IO spec. package router import ( "sync" io "verification/io" - gsync "verification/utils/ghost_sync" ) ghost +opensInvariants requires dp.Valid() requires ingressID != none[io.Ifs] requires len(oldPkt.CurrSeg.Future) > 0 @@ -51,60 +47,60 @@ requires dp.dp3s_forward( }, newPkt, egressID) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) -decreases _ -func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { - ghost ioLock.Lock() - unfold SharedInv!< dp, ioSharedArg !>() - t, s := *ioSharedArg.Place, *ioSharedArg.State - ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) - ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID}) - assert dp.dp3s_iospec_bio3s_enter_guard(s, t, pkt_internal) - unfold dp.dp3s_iospec_ordered(s, t) - unfold dp.dp3s_iospec_bio3s_enter(s, t) - io.TriggerBodyIoEnter(pkt_internal) - tN := io.CBio_IN_bio3s_enter_T(t, pkt_internal) - io.Enter(t, pkt_internal) //Event - UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) - ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) - ghost *ioSharedArg.Place = tN - fold SharedInv!< dp, ioSharedArg !>() - ghost ioLock.Unlock() +decreases +func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { + critical SharedInv! ( + unfold SharedInv!< dp, ioSharedArg !>() + t, s := *ioSharedArg.Place, *ioSharedArg.State + ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) + ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID}) + assert dp.dp3s_iospec_bio3s_enter_guard(s, t, pkt_internal) + unfold dp.dp3s_iospec_ordered(s, t) + unfold dp.dp3s_iospec_bio3s_enter(s, t) + io.TriggerBodyIoEnter(pkt_internal) + ghost tN := io.CBio_IN_bio3s_enter_T(t, pkt_internal) + io.Enter(t, pkt_internal) //Event + UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) + ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) + ghost *ioSharedArg.Place = tN + fold SharedInv!< dp, ioSharedArg !>() + ) } ghost +opensInvariants requires dp.Valid() requires ingressID == none[io.Ifs] requires egressID != none[io.Ifs] requires len(oldPkt.CurrSeg.Future) > 0 requires ElemWitness(ioSharedArg.IBufY, ingressID, oldPkt) requires dp.dp3s_forward_ext(oldPkt, newPkt, get(egressID)) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) -decreases _ -func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { - ghost ioLock.Lock() - unfold SharedInv!< dp, ioSharedArg !>() - t, s := *ioSharedArg.Place, *ioSharedArg.State - ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) - ghost pkt_internal := io.Val(io.ValInternal2{oldPkt, newPkt, get(egressID)}) - assert dp.dp3s_iospec_bio3s_exit_guard(s, t, pkt_internal) - unfold dp.dp3s_iospec_ordered(s, t) - unfold dp.dp3s_iospec_bio3s_exit(s, t) - io.TriggerBodyIoExit(pkt_internal) - tN := io.dp3s_iospec_bio3s_exit_T(t, pkt_internal) - io.Exit(t, pkt_internal) //Event - UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) - ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) - ghost *ioSharedArg.Place = tN - fold SharedInv!< dp, ioSharedArg !>() - ghost ioLock.Unlock() +decreases +func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { + critical SharedInv! ( + unfold SharedInv!< dp, ioSharedArg !>() + t, s := *ioSharedArg.Place, *ioSharedArg.State + ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) + ghost pkt_internal := io.Val(io.ValInternal2{oldPkt, newPkt, get(egressID)}) + assert dp.dp3s_iospec_bio3s_exit_guard(s, t, pkt_internal) + unfold dp.dp3s_iospec_ordered(s, t) + unfold dp.dp3s_iospec_bio3s_exit(s, t) + io.TriggerBodyIoExit(pkt_internal) + ghost tN := io.dp3s_iospec_bio3s_exit_T(t, pkt_internal) + io.Exit(t, pkt_internal) //Event + UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) + ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) + ghost *ioSharedArg.Place = tN + fold SharedInv!< dp, ioSharedArg !>() + ) } ghost +opensInvariants requires dp.Valid() requires oldPkt.LeftSeg != none[io.Seg] requires len(oldPkt.CurrSeg.Future) > 0 @@ -136,25 +132,24 @@ requires dp.dp3s_forward_xover( }, newPkt, egressID) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !> +preserves Invariant(SharedInv!) ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) -decreases _ -func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) { - ghost ioLock.Lock() - unfold SharedInv!< dp, ioSharedArg !>() - t, s := *ioSharedArg.Place, *ioSharedArg.State - ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) - ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID}) - assert dp.dp3s_iospec_bio3s_xover_guard(s, t, pkt_internal) - unfold dp.dp3s_iospec_ordered(s, t) - unfold dp.dp3s_iospec_bio3s_xover(s, t) - io.TriggerBodyIoXover(pkt_internal) - tN := io.dp3s_iospec_bio3s_xover_T(t, pkt_internal) - io.Xover(t, pkt_internal) //Event - UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) - ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) - ghost *ioSharedArg.Place = tN - fold SharedInv!< dp, ioSharedArg !>() - ghost ioLock.Unlock() +decreases +func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { + critical SharedInv! ( + unfold SharedInv!< dp, ioSharedArg !>() + t, s := *ioSharedArg.Place, *ioSharedArg.State + ApplyElemWitness(s.ibuf, ioSharedArg.IBufY, ingressID, oldPkt) + ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID}) + assert dp.dp3s_iospec_bio3s_xover_guard(s, t, pkt_internal) + unfold dp.dp3s_iospec_ordered(s, t) + unfold dp.dp3s_iospec_bio3s_xover(s, t) + io.TriggerBodyIoXover(pkt_internal) + ghost tN := io.dp3s_iospec_bio3s_xover_T(t, pkt_internal) + io.Xover(t, pkt_internal) //Event + UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt) + ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt) + ghost *ioSharedArg.Place = tN + fold SharedInv!< dp, ioSharedArg !>() + ) } \ No newline at end of file diff --git a/verification/utils/ghost_sync/ghost-mutex.gobra b/verification/utils/ghost_sync/ghost-mutex.gobra deleted file mode 100644 index e0295f43d..000000000 --- a/verification/utils/ghost_sync/ghost-mutex.gobra +++ /dev/null @@ -1,60 +0,0 @@ -// Copyright 2022 ETH Zurich -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -// +gobra - -package ghost_sync - -import "sync" -import . "verification/utils/definitions" - -// This package contains the definition of a Ghost Mutex (a.k.a. Ghost Lock), as described -// in https://arxiv.org/pdf/2311.14452. These Mutexes are used to provide a ghost-like -// interface to an invariant, for the duration of a an atomic operation. To use ghost -// mutexes soundly, we must ensure two properties: -// (1) All calls to Lock() must be acoompanied by a call to Unlock(). -// (2) All operations performed between a call to Lock() and the corresponding call to -// Unlock() must be atomic. -// Currently, Gobra does not check any of these two properties. Property (1) could be done -// by using obligations. - -type GhostMutex struct { - privateField PrivateField -} - -pred (m gpointer[GhostMutex]) LockP() -pred (m gpointer[GhostMutex]) UnlockP() - -ghost -requires acc(m.LockP(), _) -decreases _ -pure func (m gpointer[GhostMutex]) LockInv() pred() - -ghost -requires inv() && acc(m) && *m == GhostMutex{} -ensures m.LockP() && m.LockInv() == inv -decreases -func (m gpointer[GhostMutex]) SetInv(inv pred()) - -ghost -requires acc(m.LockP(), _) -ensures m.LockP() && m.UnlockP() && m.LockInv()() -decreases _ if sync.IgnoreBlockingForTermination() -func (m gpointer[GhostMutex]) Lock() - -ghost -requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()() -ensures m.LockP() -decreases _ -func (m gpointer[GhostMutex]) Unlock()