Skip to content

Commit

Permalink
Add checks for termination modulo blocking (#309)
Browse files Browse the repository at this point in the history 
* add termination checking if we ignore locking

* add termination checks modulo locking

* backup

* fix termination measure

* fix verification errors

* fix verification error
  • Loading branch information
@jcp19
jcp19 authored Apr 10, 2024
1 parent 42bde11 commit a8ff113
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 5 deletions.
25 changes: 24 additions & 1 deletion router/dataplane.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -331,6 +335,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) {
// @ preserves d.mtx.LockInv() == MutexInvariant!<d!>;
// @ 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()
Expand Down Expand Up @@ -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!<d!>;
// @ decreases 0 if sync.IgnoreBlockingForTermination()
func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error {
d.mtx.Lock()
defer d.mtx.Unlock()
Expand Down Expand Up @@ -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!<d!>;
// @ decreases 0 if sync.IgnoreBlockingForTermination()
func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error {
d.mtx.Lock()
defer d.mtx.Unlock()
Expand Down Expand Up @@ -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!<d!>()
// @ 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 {
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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!<d!>;
// @ decreases 0 if sync.IgnoreBlockingForTermination()
func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error {
d.mtx.Lock()
// @ unfold MutexInvariant!<d!>()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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!<d!>;
// @ decreases 0 if sync.IgnoreBlockingForTermination()
func (d *DataPlane) AddNextHop(ifID uint16, a *net.UDPAddr) error {
d.mtx.Lock()
defer d.mtx.Unlock()
Expand Down Expand Up @@ -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]
Expand All @@ -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))

Expand Down Expand Up @@ -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 @*/) {

Expand Down Expand Up @@ -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), _) }
Expand Down Expand Up @@ -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), _) }
Expand Down Expand Up @@ -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(), _)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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]
Expand Down
5 changes: 3 additions & 2 deletions router/svc.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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)
Expand Down
9 changes: 7 additions & 2 deletions verification/dependencies/sync/mutex.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()

0 comments on commit a8ff113

Please sign in to comment.