diff --git a/router/dataplane.go b/router/dataplane.go index f786b4213..bf9c9e371 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,27 @@ type bfdSession interface { type BatchConn interface { // @ pred Mem() + // (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.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. + // + // 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() // @ 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) @@ -166,23 +181,28 @@ 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 Prophecy(prophecyM) - // @ requires io.IOToken(place) && MultiReadBio(place, prophecyM) - // @ ensures err != nil ==> prophecyM == 0 - // @ ensures err == nil ==> prophecyM == n - // @ ensures io.IOToken(old(MultiReadBioNext(place, prophecyM))) - // @ ensures old(MultiReadBioCorrectIfs(place, prophecyM, path.IfsToIO_ifs(ingressID))) + // postconditions for IO-spec: + // @ 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) + // (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. @@ -190,17 +210,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.IOToken(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.IOToken(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 @@ -875,7 +895,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 /*@@@*/ := @@ -897,10 +917,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{dp, ioSharedArg}) // @ #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) ==> @@ -976,39 +995,16 @@ 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{dp, ioSharedArg}) // @ 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}() - // @ 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}() - // @ ioLock.Unlock() + // 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() @@ -1019,10 +1015,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 ==> @@ -1060,8 +1058,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{dp, ioSharedArg}) // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> // @ MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i] // @ invariant MultiElemWitnessWithIndex(ioSharedArg.IBufY, ioIngressID, ioValSeq, i0) @@ -1112,7 +1109,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. @@ -1191,23 +1188,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) - // @ ghost ioLock.Lock() - // @ 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}() - // @ ghost ioLock.Unlock() + // 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) @@ -1215,6 +1201,13 @@ 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)`, 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 { // @ requires err != nil && err.ErrorMem() @@ -1313,8 +1306,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{dp, ioSharedArgRun}) // @ decreases len(externals) - len(visited) for ifID, v := range externals /*@ with visited @*/ { cl := @@ -1330,18 +1322,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{dp, ioSharedArg}) + 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 @@ -1355,14 +1346,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{dp, ioSharedArg}) + 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(), _) @@ -1588,8 +1578,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{dp, ioSharedArg}) // @ 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 ==> @@ -1613,7 +1602,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 @*/) { // `oldAbsVal` is the abstract value of the packet that was received. It is // introduced here because `p.getIngressID()` is not available in the states @@ -1744,7 +1733,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ assert reveal p.scionLayer.EqPathType(p.rawPkt) // @ assert path.Type(slayers.GetPathType(p.rawPkt)) != epic.PathType // @ assert AbsIO_val(p.rawPkt, p.ingressID) == oldAbsVal - 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 @*/ @@ -1764,7 +1753,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ assert unfolding acc(p.scionLayer.Mem(p.rawPkt), R56) in slayers.CmnHdrLen <= len(p.rawPkt) // @ assert typeOf(p.scionLayer.GetPath(p.rawPkt)) == *epic.Path ==> // @ p.scionLayer.EqAbsHeader(p.rawPkt) && p.scionLayer.ValidScionInitSpec(p.rawPkt) - v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ ) + v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ 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 @*/ @@ -1938,8 +1927,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{dp, ioSharedArg}) // @ 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 ==> @@ -1962,7 +1950,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ path.IfsToIO_ifs(p.ingressID), // @ newAbsPkt.ValPkt_1) // @ 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) @@ -1976,7 +1964,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil return processResult{}, malformedPath /*@ , false, io.ValUnit{} @*/ } // @ assert p.path === p.scionLayer.GetScionPath(ub) - return p.process( /*@ ub, llIsNil, startLL, endLL , ioLock, ioSharedArg, dp @*/ ) + return p.process( /*@ ub, llIsNil, startLL, endLL, ioSharedArg, dp @*/ ) } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) @@ -2033,8 +2021,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // @ requires dp.Valid() // @ requires (typeOf(p.scionLayer.GetPath(ub)) == *epic.Path) ==> // @ p.scionLayer.EqAbsHeader(ub) && p.scionLayer.ValidScionInitSpec(ub) -// @ requires acc(ioLock.LockP(), _) -// @ requires ioLock.LockInv() == SharedInv{dp, ioSharedArg} +// @ requires Invariant(SharedInv{dp, ioSharedArg}) // @ 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 ==> @@ -2057,7 +2044,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // @ path.IfsToIO_ifs(p.ingressID), // @ newAbsPkt.ValPkt_1) // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) processEPIC( /*@ 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) processEPIC( /*@ 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 @*/) { // @ unfold acc(p.scionLayer.Mem(ub), R10) epicPath, ok := p.scionLayer.Path.(*epic.Path) if !ok { @@ -2093,7 +2080,7 @@ func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil b // @ assert p.path === p.scionLayer.GetScionPath(ub) // @ assert p.scionLayer.UBPath(ub) === ubPath - result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, llIsNil, startLL, endLL, ioLock, ioSharedArg, dp @*/ ) + result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, llIsNil, startLL, endLL, ioSharedArg, dp @*/ ) if err != nil { return result, err /*@ , addrAliases, newAbsPkt0 @*/ } @@ -4326,8 +4313,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{dp, ioSharedArg}) // @ 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 ==> @@ -4357,7 +4343,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 @*/) { @@ -4442,7 +4427,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) // The destination of the packet is this AS, so it is at the last hop of @@ -4544,9 +4529,9 @@ func (p *scionPacketProcessor) process( // @ assert nextPkt == AbsProcessEgress(AbsProcessXover(afterIngressPkt)) // @ 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) @@ -4566,9 +4551,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 971f75ff5..86400023e 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,35 +37,36 @@ pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) { // initialize the shared invariant: ghost requires io.IOToken(p) && dp.Dp3s_iospec_ordered(s, p) -ensures m.LockP() && m.LockInv() == SharedInv{dp, y} +ensures Invariant(SharedInv{dp, y}) 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}) + EstablishInvariant(SharedInv{dp, y}) + 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 +// `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) && @@ -190,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]) { 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 } diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index d4bdedd85..f19d34dd8 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" ) @@ -199,6 +198,7 @@ pure func PktUpdate(pkt io.Pkt, ingressID option[io.Ifs], egressID option[io.Ifs // 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] @@ -208,18 +208,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{dp, ioSharedArg}) 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 @@ -229,6 +228,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()) @@ -239,11 +239,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{dp, ioSharedArg}) 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) @@ -252,9 +251,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) } } @@ -262,6 +261,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() @@ -280,11 +280,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{dp, ioSharedArg}) 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) @@ -296,5 +295,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 2efb6e7f9..d7e960318 100644 --- a/router/io-spec-atomic-events.gobra +++ b/router/io-spec-atomic-events.gobra @@ -15,21 +15,16 @@ // +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 +46,60 @@ requires dp.Dp3s_forward( }, newPkt, egressID) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg} +preserves Invariant(SharedInv{dp, ioSharedArg}) 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{dp, ioSharedArg} ( + 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{dp, ioSharedArg}) 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{dp, ioSharedArg} ( + 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 +131,24 @@ requires dp.Dp3s_forward_xover( }, newPkt, egressID) -preserves acc(ioLock.LockP(), _) -preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg} +preserves Invariant(SharedInv{dp, ioSharedArg}) 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() -} \ No newline at end of file +decreases +func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) { + critical SharedInv{dp, ioSharedArg} ( + 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}() + ) +} diff --git a/verification/utils/ghost_sync/ghost-mutex.gobra b/verification/utils/ghost_sync/ghost-mutex.gobra deleted file mode 100644 index 70008d499..000000000 --- a/verification/utils/ghost_sync/ghost-mutex.gobra +++ /dev/null @@ -1,62 +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. - - -// TODO(gobra#1092): comparable -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 _ -func (m gpointer[GhostMutex]) Lock() - -ghost -requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()() -ensures m.LockP() -decreases _ -func (m gpointer[GhostMutex]) Unlock()