defer statements

A defer statement invokes a function whose execution is deferred to the moment the surrounding function returns (spec).

Defer statements are not directly related to concurrency, but we include them in this chapter because they frequently occur in concurrent code. For example, a common pattern is to defer the call of the Unlock method for a mutex. Here, we augment the SafeCounter example with a method Get:

// @ requires acc(c.Mem(), 1/4)
// @ ensures acc(c.Mem(), 1/4)
func (c *SafeCounter) Get() int {
	// @ unfold acc(c.Mem(), 1/4)
	// @ defer fold acc(c.Mem(), 1/4) // <-----
	c.mu.Lock()
	defer c.mu.Unlock() // <-----
	// @ unfold mutexInvariant!<&c.count!>()
	// @ defer fold mutexInvariant!<&c.count!>() // <-----
	return c.count
}

func client() {
	ctr := New()
	go ctr.Get()
	go ctr.Get()
	go ctr.Increment()
	go ctr.Increment()
}

We use defer three times, once deferring c.mu.Unlock() and in ghost code to defer folding the predicates mutexInvariant and c.Mem.

At the point of the defer statement, only the function and its parameters are evaluated, but the call is not yet evaluated. Deferred functions or methods are executed in the reverse order they were deferred. Gobra checks the contracts when they are executed.

For example, if we swap the order of the defer statements in the example above, Gobra reports an error since when Unlock is executed, mutexInvariant has not been folded yet.

    // ...
	// @ defer fold mutexInvariant!<&c.count!>()
	defer c.mu.Unlock()
	return c.count

ERROR  Precondition of call might not hold. 
Permission to m.LockInv()() might not suffice.