How the compiler can prove that memory safety?

Viewed 128

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?

3 Answers

Being inside a function scope gives the compiler the certainty of which operations will be executed on the struct and when. The compiler knows how structs work, and how and when (relative to the time the function is called) the code inside a function is executed.

In a global or larger scope, the compiler loses visibility over what could be modifying the memory, and when, so it cannot assure safety.

It's because of multiple threads. When "holly" is a global variable, multiple threads could access the global variable at the same time, and you are in trouble. In the case of a local variable, that variable exists once per execution of the function. If multiple threads run someFunction() simultaneously, each thread has its own "oscar" variable, so there is no chance that thread 1's "oscar" variable access thread 2's oscar variable.

An answer from Andrew_Trick on Swift Forums:

"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.

Related