diff --git a/router/dataplane.go b/router/dataplane.go index 167576808..4c9391ac5 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -104,8 +104,10 @@ type bfdSession interface { // (VerifiedSCION) an implementation must copy the fields it needs from msg // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ ensures msg.NonInitMem() + // @ decreases 0 if sync.IgnoreBlockingForTermination() ReceiveMessage(msg *layers.BFD /*@ , ghost ub []byte @*/) // @ requires acc(Mem(), _) + // @ decreases 0 if sync.IgnoreBlockingForTermination() IsUp() bool } @@ -235,6 +237,7 @@ func (e scmpError) Error() string { // @ ensures acc(d.Mem(), OutMutexPerm) // @ ensures !d.IsRunning() // @ ensures e == nil +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) SetIA(ia addr.IA) (e error) { d.mtx.Lock() defer d.mtx.Unlock() @@ -272,6 +275,7 @@ func (d *DataPlane) SetIA(ia addr.IA) (e error) { // @ ensures acc(d.Mem(), OutMutexPerm) // @ ensures !d.IsRunning() // @ ensures res == nil ==> d.KeyIsSet() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) SetKey(key []byte) (res error) { // @ share key d.mtx.Lock() @@ -331,6 +335,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // @ preserves d.mtx.LockInv() == MutexInvariant!; // @ ensures acc(d.Mem(), OutMutexPerm) // @ ensures !d.IsRunning() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { d.mtx.Lock() defer d.mtx.Unlock() @@ -367,6 +372,7 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { // @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { d.mtx.Lock() defer d.mtx.Unlock() @@ -411,6 +417,7 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error { d.mtx.Lock() defer d.mtx.Unlock() @@ -448,6 +455,7 @@ func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error { // (VerifiedSCION) unlike all other setter methods, this does not lock d.mtx. // This was reported in https://github.com/scionproto/scion/issues/4282. // @ preserves MutexInvariant!() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddLinkType(ifID uint16, linkTo topology.LinkType) error { // @ unfold acc(d.Mem(), OutMutexPerm) if _, existsB := d.linkTypes[ifID]; existsB { @@ -504,6 +512,7 @@ func (d *DataPlane) AddExternalInterfaceBFD(ifID uint16, conn BatchConn, // returns InterfaceUp if the relevant bfdsession state is up, or if there is no BFD // session. Otherwise, it returns InterfaceDown. // @ preserves acc(d.Mem(), R5) +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) getInterfaceState(interfaceID uint16) control.InterfaceState { // @ unfold acc(d.Mem(), R5) // @ defer fold acc(d.Mem(), R5) @@ -564,6 +573,7 @@ func (d *DataPlane) addBFDController(ifID uint16, s *bfdSend, cfg control.BFD, // @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { d.mtx.Lock() // @ unfold MutexInvariant!() @@ -616,6 +626,7 @@ func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { // @ requires a != nil && acc(a.Mem(), R10) // @ preserves acc(d.Mem(), OutMutexPerm/2) // @ preserves d.mtx.LockP() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { d.mtx.Lock() defer d.mtx.Unlock() @@ -646,6 +657,7 @@ func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { // @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) AddNextHop(ifID uint16, a *net.UDPAddr) error { d.mtx.Lock() defer d.mtx.Unlock() @@ -915,11 +927,13 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ invariant processor.sInit() && processor.sInitD() === d + // @ decreases pkts - i0 for i0 := 0; i0 < pkts; i0++ { // @ assert &msgs[:pkts][i0] == &msgs[i0] // @ preserves 0 <= i0 && i0 < pkts && pkts <= len(msgs) // @ preserves acc(msgs[i0].Mem(), R1) // @ ensures p === msgs[:pkts][i0].GetMessage() + // @ decreases // @ outline( // @ unfold acc(msgs[i0].Mem(), R1) p := msgs[:pkts][i0] @@ -936,7 +950,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta // @ prometheus.CounterMemImpliesNonNil(inputCounters.InputBytesTotal) inputCounters.InputPacketsTotal.Inc() // @ assert msgs[i0].GetN() == p.N - // (VerifiedSCION) Gobra still does not fully support floats // @ fl.CastPreservesOrder64(0, p.N) inputCounters.InputBytesTotal.Add(float64(p.N)) @@ -1353,6 +1366,7 @@ func (p *scionPacketProcessor) reset() (err error) { // @ ensures respr.OutPkt !== rawPkt && respr.OutPkt != nil ==> // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) processPkt(rawPkt []byte, srcAddr *net.UDPAddr) (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { @@ -1499,6 +1513,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ ensures acc(&p.ingressID, R20) // @ ensures p.bfdLayer.NonInitMem() // @ ensures err != nil ==> err.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (err error) { // @ unfold acc(p.d.Mem(), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } @@ -1534,6 +1549,7 @@ func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (er // @ ensures p.bfdLayer.NonInitMem() // @ ensures sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures res != nil ==> res.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ unfold acc(p.d.Mem(), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } @@ -1563,6 +1579,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ invariant m != nil ==> acc(m, R20) // @ invariant m != nil ==> forall a *net.UDPAddr :: { a in range(m) } a in range(m) ==> acc(a.Mem(), _) // @ invariant acc(&p.srcAddr, R20) && acc(p.srcAddr.Mem(), _) + // @ decreases len(p.d.internalNextHops) - len(keys) for k, v := range p.d.internalNextHops /*@ with keys @*/ { // @ assert acc(&p.d.internalNextHops, _) // @ assert forall a *net.UDPAddr :: { a in range(m) } a in range(m) ==> acc(a.Mem(), _) @@ -1629,6 +1646,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { var ok bool @@ -2242,6 +2260,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e // @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> !addrAliasesUb // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) (resaddr *net.UDPAddr, respr processResult, reserr error /*@ , addrAliasesUb bool @*/) { // (VerifiedSCION) the parameter used to be p.scionLayer, // instead of &p.scionLayer. @@ -2403,6 +2422,7 @@ func (p *scionPacketProcessor) egressInterface() uint16 { // @ ensures respr.OutPkt != nil ==> // @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr error) { egressID := p.egressInterface() // @ p.d.getBfdSessionsMem() @@ -2715,6 +2735,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error /*@, addrAliasesPkt bool @*/) { if r, err := p.parsePath( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) @@ -2867,6 +2888,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ ensures respr.OutPkt !== p.rawPkt && respr.OutPkt != nil ==> // @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { // @ ghost ubScionL := p.rawPkt // @ p.scionLayer.ExtractAcc(ubScionL) @@ -3063,6 +3085,7 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error / // (VerifiedSCION) the type of 's' was changed from slayers.SCION to *slayers.SCION. This makes // specs a lot easier and, makes the implementation faster as well by avoiding passing large data-structures // by value. We should consider porting merging this in upstream SCION. +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (d *DataPlane) resolveLocalDst(s *slayers.SCION /*@, ghost ub []byte @*/) (resaddr *net.UDPAddr, reserr error /*@ , addrAliasesUb bool @*/) { // @ ghost start, end := s.ExtractAcc(ub) // @ assert s.RawDstAddr === ub[start:end] diff --git a/router/svc.go b/router/svc.go index 2f84ec164..8c8fd62bc 100644 --- a/router/svc.go +++ b/router/svc.go @@ -42,6 +42,7 @@ func newServices() (s *services) { // @ preserves acc(s.Mem(), R50) // @ requires acc(a.Mem(), R10) +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) { //@ unfold acc(s.Mem(), R50) s.mtx.Lock() @@ -69,6 +70,7 @@ func (s *services) AddSvc(svc addr.HostSVC, a *net.UDPAddr) { // @ preserves acc(s.Mem(), R50) // @ preserves acc(a.Mem(), R10) +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (s *services) DelSvc(svc addr.HostSVC, a *net.UDPAddr) { //@ unfold acc(s.Mem(), R50) s.mtx.Lock() @@ -102,6 +104,7 @@ func (s *services) DelSvc(svc addr.HostSVC, a *net.UDPAddr) { // @ requires acc(s.Mem(), _) // @ ensures !b ==> r == nil // @ ensures b ==> acc(r.Mem(), _) +// @ decreases 0 if sync.IgnoreBlockingForTermination() func (s *services) Any(svc addr.HostSVC) (r *net.UDPAddr, b bool) { //@ unfold acc(s.Mem(), _) s.mtx.Lock() @@ -130,8 +133,6 @@ func (s *services) Any(svc addr.HostSVC) (r *net.UDPAddr, b bool) { // @ ensures b ==> 0 < len(addrs) // @ ensures b ==> 0 <= res && res < len(addrs) // @ ensures !b ==> res == -1 -// We could ensure stronger postconditions for this method, -// but it is unclear right now if we need them. // @ decreases func (s *services) index(a *net.UDPAddr, addrs []*net.UDPAddr /*@ , ghost k addr.HostSVC @*/) (res int, b bool) { // @ unfold acc(validMapValue(k, addrs), R11) diff --git a/verification/dependencies/sync/mutex.gobra b/verification/dependencies/sync/mutex.gobra index feb75100e..7b18c6566 100644 --- a/verification/dependencies/sync/mutex.gobra +++ b/verification/dependencies/sync/mutex.gobra @@ -25,11 +25,16 @@ ensures m.LockP() && m.LockInv() == inv decreases func (m *Mutex) SetInv(ghost inv pred()) +ghost +decreases _ +pure func IgnoreBlockingForTermination() bool + requires acc(m.LockP(), _) -ensures m.LockP() && m.UnlockP() && m.LockInv()() +ensures m.LockP() && m.UnlockP() && m.LockInv()() +decreases _ if IgnoreBlockingForTermination() func (m *Mutex) Lock() requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()() ensures m.LockP() -decreases +decreases _ func (m *Mutex) Unlock()