How the compiler can prove that memory safety?

When I read The Swift Programming Language: Memory Safety, I was confused by the section Conflicting Access to Properties:

The code below shows that the same error appears for overlapping write
accesses to the properties of a structure that’s stored in a global
variable.

var holly = Player(name: "Holly", health: 10, energy: 10)
balance(&holly.health, &holly.energy)  // Error 

In practice,
most access to the properties of a structure can overlap safely. For
example, if the variable holly in the example above is changed to a
local variable instead of a global variable, the compiler can prove
that overlapping access to stored properties of the structure is
safe:

func someFunction() {
    var oscar = Player(name: "Oscar", health: 10, energy: 10)
    balance(&oscar.health, &oscar.energy)  // OK 
}

In the example above, Oscar’s health and energy are passed as the two in-out parameters to balance(_:_:). The compiler can prove that memory
safety is preserved because the two stored properties don’t interact
in any way.

How the compiler can prove that memory safety?

1 Like

"don't interact" is a strong statement. The compiler simply checks that each access to 'oscar' in the call to 'balance' can only modify independent pieces of memory ('heath' vs 'energy'). This is a special case because any access to a struct is generally modeled as a read/write to the entire struct value. The compiler does a little extra work to detect and allow this special case because copying the 'oscar' struct in situations like this would be inconvenient.

3 Likes

It also has to do with the scope & lifetime of the memory in use here.

As a global variable in the first example, theoretically multiple concurrent use of the same variables can happen to the same object in memory.

In the second example, it is a local variable to a function so only the given function call has access to that object in memory (even if multiple calls happen concurrently - each call has its own instance), and that the inout references to different properties of said object are completely isolated.