From 4f6b5e36f92ff2f7b2be1e0719d7aa9777d4a33e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 25 Jan 2026 19:50:20 +0100 Subject: [PATCH 1/6] remove ghost Mutex, change to invariants --- router/dataplane.go | 82 +++++------ router/dataplane_concurrency_model.gobra | 12 +- router/io-spec-abstract-transitions.gobra | 27 ++-- router/io-spec-atomic-events.gobra | 127 +++++++++--------- .../utils/ghost_sync/ghost-mutex.gobra | 60 --------- 5 files changed, 116 insertions(+), 192 deletions(-) delete mode 100644 verification/utils/ghost_sync/ghost-mutex.gobra 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() From 0e12fb7d91a49a086ff91215b06f576b80d3302f Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 12:03:56 +0000 Subject: [PATCH 2/6] Do not require ReadBatch and WriteBatch to be atomic Gobra does not allow interface methods to be marked as `atomic`, so calls to `BatchConn.ReadBatch` and `BatchConn.WriteBatch` may not occur inside a critical region. As a consequence, the caller can no longer perform the transitions of the IO specification atomically with the physical read/write. Instead, we now assume that both methods open the shared invariant themselves and perform the corresponding transitions internally, atomically with the respective physical operation. Their contracts take `Invariant(SharedInv{...})` instead of the `io.token` and, in exchange: - `ReadBatch` returns the sequence of abstract values of the packets that were received together with a witness for each of them, which makes the prophecy over the number of received packets unnecessary; - `WriteBatch` requires the witness that the packet being sent is in the output buffer of the model, which is what is needed to establish the guard of the `send` transition. The `MultiReadBio` definitions are kept, as they specify the effect that `ReadBatch` is assumed to have on the shared invariant. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4 --- router/dataplane.go | 107 ++++++++++------------- router/dataplane_concurrency_model.gobra | 25 +++--- router/io-spec-atomic-events.gobra | 2 +- 3 files changed, 61 insertions(+), 73 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 0c4896667..229136c04 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -148,15 +148,23 @@ type bfdSession interface { type BatchConn interface { // @ pred Mem() - // @ atomic + // (VerifiedSCION) Gobra does not allow interface methods to be marked as `atomic`, so a + // call to `ReadBatch` may not occur inside a critical region and, thus, the caller cannot + // perform the `recv` transitions of the IO specification atomically with the physical read. + // Instead, we assume here that `ReadBatch` performs them itself: for every packet that it + // receives, it opens the shared invariant `SharedInv{dp, ioSharedArg}` and performs the + // corresponding `recv` transition atomically with the physical reception of that packet. + // This is why the contract below takes the invariant (instead of the `io.token` and the + // `MultiReadBio` permissions, which are now held by the invariant throughout the call) and, + // in exchange, yields the sequence `ioValSeq` with the abstract values of the packets that + // were received, together with a witness for each of them. Notice that this models the + // underlying socket more faithfully than treating the entire batch read as a single atomic + // operation, given that the packets of a batch are genuinely received one at a time. // @ 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) @@ -170,21 +178,29 @@ type BatchConn interface { // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ ensures err != nil ==> err.ErrorMem() // contracts for IO-spec - // @ ensures err != nil ==> prophecyM == 0 - // @ ensures err == nil ==> prophecyM == n - // @ ensures io.token(old(MultiReadBioNext(place, prophecyM))) - // @ ensures old(MultiReadBioCorrectIfs(place, prophecyM, path.ifsToIO_ifs(ingressID))) + // @ requires dp.Valid() + // @ preserves Invariant(SharedInv{dp, ioSharedArg}) + // @ ensures err == nil ==> len(ioValSeq) == n + // @ ensures err == nil ==> + // @ MultiElemWitness(ioSharedArg.IBufY, path.ifsToIO_ifs(ingressID), ioValSeq) // @ ensures err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> - // @ MsgToAbsVal(&msgs[i], ingressID) == old(MultiReadBioIO_val(place, n)[i]) - ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error) + // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] + ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) (n int, err error /*@, ghost ioValSeq seq[io.Val] @*/) // @ requires acc(addr.Mem(), _) // @ requires acc(Mem(), _) // @ preserves acc(sl.Bytes(b, 0, len(b)), R10) // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) - // @ atomic + // (VerifiedSCION) As for `ReadBatch`, `WriteBatch` cannot be marked as `atomic` because it + // is an interface method. We assume instead that it opens the shared invariant + // `SharedInv{dp, ioSharedArg}` itself and performs the `send` transition of the IO + // specification atomically with the physical write. The `ElemWitness` required below is + // what an implementation needs in order to establish the guard of that transition, namely + // that the packet being sent is in the output buffer of the model. The transition is + // performed even when the write fails; otherwise, the router could not continue after + // failing to send a packet. // @ requires acc(Mem(), _) // (VerifiedSCION) opted for less reusable spec for WriteBatch for // performance reasons. @@ -192,17 +208,17 @@ type BatchConn interface { // @ requires acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr() // @ requires acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50) // preconditions for IO-spec: + // @ requires dp.Valid() // @ requires MsgToAbsVal(&msgs[0], egressID) == ioAbsPkts - // @ requires io.token(place) && io.CBioIO_bio3s_send(place, ioAbsPkts) + // @ requires ioAbsPkts.isValPkt || ioAbsPkts.isValUnsupported + // @ requires ioAbsPkts.isValPkt ==> + // @ ElemWitness(ioSharedArg.OBufY, ioAbsPkts.ValPkt_1, ioAbsPkts.ValPkt_2) + // @ preserves Invariant(SharedInv{dp, ioSharedArg}) // @ ensures acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr() // @ ensures acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() - // postconditions for IO-spec: - // (VerifiedSCION) the permission to the protocol must always be returned, - // otherwise the router cannot continue after failing to send a packet. - // @ ensures io.token(old(io.dp3s_iospec_bio3s_send_T(place, ioAbsPkts))) - WriteBatch(msgs underlayconn.Messages, flags int /*@, ghost egressID uint16, ghost place io.Place, ghost ioAbsPkts io.Val @*/) (n int, err error) + WriteBatch(msgs underlayconn.Messages, flags int /*@, ghost egressID uint16, ghost ioAbsPkts io.Val, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) (n int, err error) // @ requires Mem() // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -973,34 +989,12 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant d.DpAgreesWithSpec(dp) && dp.Valid() for d.running { // @ ghost ioIngressID := path.ifsToIO_ifs(ingressID) - // Multi recv event - // @ critical SharedInv{dp, ioSharedArg} ( - // @ unfold SharedInv{dp, ioSharedArg}() - // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State - // @ ghost numberOfReceivedPacketsProphecy := AllocProphecy() - // @ ExtractMultiReadBio(dp, t, numberOfReceivedPacketsProphecy, s) - // @ MultiUpdateElemWitness(t, numberOfReceivedPacketsProphecy, ioIngressID, s, ioSharedArg) - // @ ghost ioValSeq := MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy) - - // @ ghost sN := MultiReadBioUpd(t, numberOfReceivedPacketsProphecy, s) - // @ ghost tN := MultiReadBioNext(t, numberOfReceivedPacketsProphecy) - // @ assert dp.dp3s_iospec_ordered(sN, tN) - // @ BeforeReadBatch: - pkts, err := rd.ReadBatch(msgs /*@, ingressID, numberOfReceivedPacketsProphecy, t @*/) - // @ assert old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)) == ioValSeq - // @ assert err == nil ==> - // @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> - // @ ioValSeq[i] == old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)[i]) - // @ assert err == nil ==> - // @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] - // @ ghost *ioSharedArg.State = sN - // @ ghost *ioSharedArg.Place = tN - // @ assert err == nil ==> - // @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> - // @ MsgToAbsVal(&msgs[i], ingressID) == old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)[i]) - // @ MultiElemWitnessConv(ioSharedArg.IBufY, ioIngressID, ioValSeq) - // @ fold SharedInv{dp, ioSharedArg}() - // @ ) + // Multi recv event. + // The `recv` transitions of the IO specification are performed inside + // `ReadBatch`, which opens the shared invariant itself (cf. the comment on + // the contract of `BatchConn.ReadBatch`). This is why no critical region is + // opened here. + pkts, err /*@, ioValSeq @*/ := rd.ReadBatch(msgs /*@, ingressID, ioSharedArg, dp @*/) // End of multi recv event // @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() @@ -1011,10 +1005,12 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // error metric continue } + // @ MultiElemWitnessConv(ioSharedArg.IBufY, ioIngressID, ioValSeq) if pkts == 0 { continue } // @ assert pkts <= len(msgs) + // @ assert pkts == len(ioValSeq) // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> // @ !msgs[i].HasWildcardPermAddr() // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> @@ -1182,23 +1178,12 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ absIO_val(writeMsgs[0].Buffers[0], result.EgressID) // @ assert result.OutPkt != nil ==> newAbsPkt == // @ absIO_val(writeMsgs[0].Buffers[0], result.EgressID) + // @ assert newAbsPkt.isValPkt || newAbsPkt.isValUnsupported // @ fold acc(writeMsgs[0].Mem(), R50) - // @ critical SharedInv{dp, ioSharedArg} ( - // @ unfold SharedInv{dp, ioSharedArg}() - // @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State - // @ ghost if(newAbsPkt.isValPkt) { - // @ ApplyElemWitness(s.obuf, ioSharedArg.OBufY, newAbsPkt.ValPkt_1, newAbsPkt.ValPkt_2) - // @ assert newAbsPkt.ValPkt_2 elem AsSet(s.obuf[newAbsPkt.ValPkt_1]) - // @ assert dp.dp3s_iospec_bio3s_send_guard(s, t, newAbsPkt) - // @ } else { assert newAbsPkt.isValUnsupported } - // @ unfold dp.dp3s_iospec_ordered(s, t) - // @ unfold dp.dp3s_iospec_bio3s_send(s, t) - // @ io.TriggerBodyIoSend(newAbsPkt) - // @ ghost tN := io.dp3s_iospec_bio3s_send_T(t, newAbsPkt) - _, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT /*@, result.EgressID, t, newAbsPkt @*/) - // @ ghost *ioSharedArg.Place = tN - // @ fold SharedInv{dp, ioSharedArg}() - // @ ) + // The `send` transition of the IO specification is performed inside + // `WriteBatch` (cf. the comment on the contract of `BatchConn.WriteBatch`), + // which is why no critical region is opened here. + _, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT /*@, result.EgressID, newAbsPkt, ioSharedArg, dp @*/) // @ 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) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 12f65cdd0..ce7526190 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -53,18 +53,21 @@ func InitSharedInv( return y } -/////////////////////////////////////// Prophecies /////////////////////////////////////// -// To establish permission for incoming packets, we need to predict the quantity. -// The return value of AllocProphecy is assumed to be identical to the actual number -// of received packets. -pred Prophecy(int) - -ghost -ensures 0 <= expectedPkts && Prophecy(expectedPkts) -decreases -func AllocProphecy() (expectedPkts int) - /////////////////////////////////////// MultiBio /////////////////////////////////////// +// The definitions in this section describe the effect that receiving a batch of +// `expectedPkts` packets has on the state of the model: `MultiReadBio` is the permission to +// perform that many consecutive `recv` transitions, `MultiReadBioNext` and `MultiReadBioUpd` +// compute the place and the local state that result from performing them, and +// `MultiReadBioIO_val` collects the abstract values of the packets that are received. +// +// Because Gobra does not allow interface methods to be marked as `atomic`, these transitions +// can no longer be performed by the caller of `BatchConn.ReadBatch` while holding the shared +// invariant open; they are instead assumed to be performed inside `ReadBatch` itself (see the +// comment on its contract). These definitions remain here because they specify precisely the +// effect that `ReadBatch` is assumed to have on the shared invariant, and because +// `ExtractMultiReadBio` and `MultiUpdateElemWitness` below show that every step of that effect, +// except for the `recv` events themselves (which *are* the physical read), follows from the +// shared invariant alone. pred MultiReadBio(ghost t io.Place, ghost expectedPkts int) { (expectedPkts > 0 ==> io.CBioIO_bio3s_recv(t) && diff --git a/router/io-spec-atomic-events.gobra b/router/io-spec-atomic-events.gobra index 9408feafa..7d2e7af86 100644 --- a/router/io-spec-atomic-events.gobra +++ b/router/io-spec-atomic-events.gobra @@ -151,4 +151,4 @@ func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressI ghost *ioSharedArg.Place = tN fold SharedInv{dp, ioSharedArg}() ) -} \ No newline at end of file +} From ec283f61ac9174b8dfde275f919e9d87de1a6155 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 12:30:32 +0000 Subject: [PATCH 3/6] Extract the recv permission reasoning into a lemma `ExtractRecvPermissions` shows that the permission to receive an arbitrary number of packets can always be extracted from the IO permissions held by the shared invariant, together with the resulting place and local state and a witness for every received packet. This is the ghost code that used to be inlined in the critical region around `ReadBatch`. It now states the proof obligation underlying the IO specification assumed for `BatchConn.ReadBatch`: everything that `ReadBatch` is assumed to do to the shared invariant follows from the invariant alone, except for advancing the IO token, which is the physical reception of the packets. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4 --- router/dataplane.go | 3 ++ router/dataplane_concurrency_model.gobra | 48 ++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 229136c04..f3d935a14 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -160,6 +160,9 @@ type BatchConn interface { // were received, together with a witness for each of them. Notice that this models the // underlying socket more faithfully than treating the entire batch read as a single atomic // operation, given that the packets of a batch are genuinely received one at a time. + // + // The lemma `ExtractRecvPermissions` discharges every part of this assumption except for + // advancing the IO token, which is the physical reception of the packets. // @ requires acc(Mem(), _) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index ce7526190..900460aa5 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -65,9 +65,8 @@ func InitSharedInv( // invariant open; they are instead assumed to be performed inside `ReadBatch` itself (see the // comment on its contract). These definitions remain here because they specify precisely the // effect that `ReadBatch` is assumed to have on the shared invariant, and because -// `ExtractMultiReadBio` and `MultiUpdateElemWitness` below show that every step of that effect, -// except for the `recv` events themselves (which *are* the physical read), follows from the -// shared invariant alone. +// `ExtractRecvPermissions` below discharges every part of that effect that does not require +// physically receiving a packet. pred MultiReadBio(ghost t io.Place, ghost expectedPkts int) { (expectedPkts > 0 ==> io.CBioIO_bio3s_recv(t) && @@ -191,6 +190,49 @@ func MultiUpdateElemWitness( } } +// Shows that the permission to receive an arbitrary number `n` of packets can always be +// extracted from the IO permissions of the shared invariant. Given the contents of +// `SharedInv{dp, y}` for the place `t` and the local state `s`, this lemma yields the permission +// to perform `n` consecutive `recv` transitions, the abstract values `ioValSeq` of the packets +// that are received, the place `tN` and the local state `sN` that result from performing them, +// and, provided that all of these packets are received from the interface `k`, a witness for +// every one of them. Notice that the invariant cannot be closed again by this lemma, as the IO +// token is still at the place `t`; that is why the lemma operates on the contents of the +// invariant instead of on `Invariant(SharedInv{dp, y})` itself. +// +// This lemma is the proof obligation underlying the IO specification that is assumed for +// `BatchConn.ReadBatch` (cf. the comment on its contract): every part of the effect that +// `ReadBatch` is assumed to have on the shared invariant follows from the invariant alone, +// with the single exception of advancing the IO token from `t` to `tN`, which is the physical +// reception of the packets and thus cannot be discharged by a ghost lemma. The lemma is not +// applied by the router itself, because `ReadBatch` may not be marked as `atomic` and thus +// performs all of these steps internally. +ghost +requires 0 <= n +requires dp.dp3s_iospec_ordered(s, t) +requires ElemAuth(s.ibuf, y.IBufY) && ElemAuth(s.obuf, y.OBufY) +ensures MultiReadBio(t, n) +ensures sN == MultiReadBioUpd(t, n, s) +ensures tN == MultiReadBioNext(t, n) +ensures ioValSeq == MultiReadBioIO_val(t, n) && len(ioValSeq) == n +ensures dp.dp3s_iospec_ordered(sN, tN) +ensures ElemAuth(sN.ibuf, y.IBufY) && ElemAuth(sN.obuf, y.OBufY) +ensures MultiReadBioCorrectIfs(t, n, k) ==> MultiElemWitness(y.IBufY, k, ioValSeq) +decreases +func ExtractRecvPermissions( + dp io.DataPlaneSpec, + t io.Place, + n int, + s io.Dp3sStateLocal, + k Key, + y SharedArg) (ioValSeq seq[io.Val], sN io.Dp3sStateLocal, tN io.Place) { + ExtractMultiReadBio(dp, t, n, s) + MultiUpdateElemWitness(t, n, k, s, y) + ioValSeq = MultiReadBioIO_val(t, n) + sN = MultiReadBioUpd(t, n, s) + tN = MultiReadBioNext(t, n) +} + // Every well-formed packet is accompanied by a witness. Establishing the MultiElemWitness // predicate recursively is easier, but working with an index is more convenient. pred MultiElemWitness(ghost y ElemRA, ghost k Key, ghost es seq[io.Val]) { From 66f99a74877e8518af1e48573f7148d373deae2b Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 15:01:20 +0000 Subject: [PATCH 4/6] Stabilize the fold of writeMsgInv after WriteBatch The OOB buffers of both the read and the write messages are nil, so all of their Mem() instances and writeMsgInv share the single predicate instance sl.Bytes(nil, 0, 0). After merging master, Gobra stopped being able to add up the shares of that instance held at the end of the loop body and reported that the permission for the fold might not suffice, even though the same fold verifies on both parents of the merge. Provide a fresh instance with sl.NilAcc_Bytes() before the fold, as is already done earlier in the same block. This is sound: the body of sl.Bytes is vacuous for an empty slice, so the instance protects no memory. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4 --- router/dataplane.go | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/router/dataplane.go b/router/dataplane.go index 56d9056d1..2bbf95569 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1202,6 +1202,12 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) // @ msgs[:pkts][i0].IsActive = false // @ fold msgs[:pkts][i0].Mem() + // (VerifiedSCION) The OOB buffers of `msgs` and of `writeMsgs` are all nil, so + // every `Mem()` instance above and `writeMsgInv` share the single instance + // `sl.Bytes(nil, 0, 0)`. Gobra occasionally fails to add up the shares of that + // instance that are held here; the call below provides a fresh one, which is + // sound because the predicate protects no memory when the slice is empty. + // @ sl.NilAcc_Bytes() // @ fold writeMsgInv(writeMsgs) if err != nil { // @ requires err != nil && err.ErrorMem() From aff08d303951bb1d208e85bbb379bae51ccc7431 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 6 Sep 2026 16:42:36 +0000 Subject: [PATCH 5/6] Raise the assertion timeout of the router package After merging master, the verification of Run keeps failing on a single permission check, but not always on the same one: first on the fold of writeMsgInv at the end of the loop body, and then, once an extra share of sl.Bytes(nil, 0, 0) was made available there, on the sl.Bytes(ubuf, ...) conjunct of the loop invariant. Making more permission available cannot make a permission check fail, so neither of these is a genuine shortfall; they are assertions that exceed the 45s assert timeout, and which one tips over varies with unrelated perturbations of the proof. Both parents of the merge verify, so raise the timeout for this package rather than weakening any specification. Only assertions that would otherwise be reported as failures are affected, so the effect on the running time of the job is bounded by a couple of minutes. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4 --- router/dataplane.go | 7 ++++--- router/gobra.json | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 2bbf95569..a3095794b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1204,9 +1204,10 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ fold msgs[:pkts][i0].Mem() // (VerifiedSCION) The OOB buffers of `msgs` and of `writeMsgs` are all nil, so // every `Mem()` instance above and `writeMsgInv` share the single instance - // `sl.Bytes(nil, 0, 0)`. Gobra occasionally fails to add up the shares of that - // instance that are held here; the call below provides a fresh one, which is - // sound because the predicate protects no memory when the slice is empty. + // `sl.Bytes(nil, 0, 0)`, of which we hold the two symbolic shares R50 and + // 1-R50 at this point. The call below makes a full share available directly, + // which keeps the fold below from timing out. It is sound because the body of + // `sl.Bytes` is vacuous for an empty slice. // @ sl.NilAcc_Bytes() // @ fold writeMsgInv(writeMsgs) if err != nil { diff --git a/router/gobra.json b/router/gobra.json index e8e772b43..8dfeccdab 100644 --- a/router/gobra.json +++ b/router/gobra.json @@ -3,5 +3,6 @@ "mce_mode": "on", "more_joins": "impure", "conditionalize_permissions": true, - "parallelize_branches": false + "parallelize_branches": false, + "assert_timeout": 120000 } From 1536d6085eb1edeb934e185fd1c04dc57a60d5cd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 7 Sep 2026 07:06:17 +0000 Subject: [PATCH 6/6] Address review: trim comment and group the IO clauses of ReadBatch Move the IO preconditions of ReadBatch right after its other preconditions and its IO postconditions right after its other postconditions, matching the layout already used by WriteBatch. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RtaS6t2NWpe3WRn6w9gXz4 --- router/dataplane.go | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index a3095794b..bf9c9e371 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -157,9 +157,7 @@ type BatchConn interface { // This is why the contract below takes the invariant (instead of the `io.IOToken` and the // `MultiReadBio` permissions, which are now held by the invariant throughout the call) and, // in exchange, yields the sequence `ioValSeq` with the abstract values of the packets that - // were received, together with a witness for each of them. Notice that this models the - // underlying socket more faithfully than treating the entire batch read as a single atomic - // operation, given that the packets of a batch are genuinely received one at a time. + // were received, together with a witness for each of them. // // The lemma `ExtractRecvPermissions` discharges every part of this assumption except for // advancing the IO token, which is the physical reception of the packets. @@ -168,6 +166,9 @@ type BatchConn interface { // @ msgs[i].Mem() // @ requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) + // preconditions for IO-spec: + // @ requires dp.Valid() + // @ preserves Invariant(SharedInv{dp, ioSharedArg}) // @ 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) @@ -180,9 +181,7 @@ type BatchConn interface { // @ ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> // @ sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer())) // @ ensures err != nil ==> err.ErrorMem() - // contracts for IO-spec - // @ requires dp.Valid() - // @ preserves Invariant(SharedInv{dp, ioSharedArg}) + // postconditions for IO-spec: // @ ensures err == nil ==> len(ioValSeq) == n // @ ensures err == nil ==> // @ MultiElemWitness(ioSharedArg.IBufY, path.IfsToIO_ifs(ingressID), ioValSeq)