Guardian's Safe Concurrency Model

Instead of using traditional locks, synchronization in Guardian is done with Guards via the Guard, GuardVar, and Cond types. You can read more about those types in their respective sections. Guards are a low-level synchronization primitive with an asynchronous, continuation-based interface. They are fast, immune to deadlocks, make efficient use of threads, and can be used to implement a variety of synchronization patterns. Despite their benefits, Guards tend to beget a programming style which is different from traditional lock-based programming, requires discipline to ensure correctness, and tends to look rather ugly in more traditional languages. Guardian itself is focused on providing an environment which makes programming with Guards easier, prettier, safer, and more productive.

This page will explain the core concepts of the Guardian concurrency model.

Sharing Data Between Threads

Guardian imposes rules regarding how we are allowed to share data between threads. In Guardian, the root of all parallelism is the Pool::run() function. This function accepts a closure which is run in a new thread (more precisely, submitted to the thread pool). Any function that provides parallelism, whether it lie in the standard library or in user code, must by definition package its asynchronous work into a closure and call Pool::run(). This implies that the only way for data to be visible to multiple threads is for it to be captured by a closure.

Lexical vs. Temporal Scoping

As a programmer, you should be familiar with the concept of lexical scoping. Just in case, here's a quick example---consider the following Java code:

public static void main(String[] args) { // Begin scope '1
    int a = 2;

    if (a > 0) { // Begin scope '2
        int b = 5;
        int c = a + b;
        
        // a, b, and c are all visible here
        System.out.println("a = " + a);
        System.out.println("b = " + b);
        System.out.println("a + b = " + c);
    } // End scope '2
    
    // Only a is visible here
    System.out.println("a = " + a);
} // End scope '1

Each matched pair of curly braces forms a new lexical scope which is nested inside the scope that encloses it. Any variable declared inside a scope is visible to all code in that scope, as well as in any child scopes, but not in the parent scope. Put another way, visibility in a lexical scope propagates "downwards" to all scopes that are nested inside it, but not "upwards" to the scope in which it is nested.

In an abstract sense, code is executed in the order it is written. In reality, both compilers and hardware (1, 2) are allowed to, and aggressively do, execute things out of the written order for performance reasons. In a single-threaded context, this is done in a way which is completely transparent to the programmer, who can blissfully pretend that the CPU really is executing their code in the written order. In a parallel context, however, this is not the case; without proper synchronization, the CPU is allowed to do all kinds of wonky things to our code that make it behave in completely unreasonable ways. This is one of the main reasons why parallel programming is so challenging.

To make discussing these matters simpler, it is important to distinguish between order of execution in the sense of the abstract machine, which governs the way we model and reason about the execution of code in our brains; and order of execution in the sense of the physical machine, which reflects the reality of what the CPU is actually doing. In a single-threaded environment, or even in a parallel context without shared memory, we as programmers can ignore this distinction because the instruction reordering is done in a way that preserves equivalence in behavior between the two models. When we perform synchronization in a parallel context with shared memory, we are, in essence, imposing a restriction upon the order of execution in both the abstract and physical models.

We do not require anything close to complete knowledge of the physical execution order when making synchronization decisions in our parallel programs. However, we do need a firm grasp on the kinds of uncertainty which are introduced into the abstract execution order by parallelism, as well as the specific effect each particular synchronization pattern has on this uncertainty. Too much uncertainty causes unsoundness, and synchronization reduces uncertainty, but more uncertainty is indicative of more parallelism and therefore higher performance. Accordingly, we want to be surgical about where and to what degree we apply synchronization.

To encapsulate the level of knowledge about the execution order needed to make sound synchronization decisions, Guardian introduces the concept of temporal scoping. Like lexical scoping, temporal scoping is a way of modeling the visibility of variables in a program. In Guardian, the code in a particular temporal scope is guaranteed to comprise an atomic, linearizable operation. This has three important implications:

• In the abstract sense, all code in a particular temporal scope is guaranteed to execute in the order it appears in the source code.
• In the abstract sense, each temporal scope either strictly precedes or strictly follows each of the other temporal scopes. In other words, all temporal scopes in the program are guaranteed to form a single total order.
• In the physical sense, all code observes a consistent view of the program state!

In summary, Guardian's temporal scoping model serves as the backbone for its concurrency safety guarantees by providing a unified way for both the compiler and human programmers to reason about the order of execution in their programs.

Temporal Scoping Rules in Guardian

In Guardian, closures form temporal scopes. Closures which represent a unit of asynchronous work are called tasks. The only exception is the entry function, which forms its own special temporal scope. Like in most other languages that support closures, variables that are visible to the enclosing scope can be captured by the closure. This means that the closure will own references to the captured variables which are visible to the code inside the closure, even if they go out of scope by the time the closure is executed. In Guardian, the compiler deduces which variables to capture by examining the code inside the closure, but there are certain rules regarding which types of variables can be captured. In general, the following rules apply:

• Immutable data can always be captured.
• Mutable data can only be captured if one of the following conditions is met:
  • The data is behind a unique reference. In this case, the variable will be "captured by move," meaning that the enclosing scope will lose access to the data at the lexical position where the closure is defined.
  • The data is enclosed in a type which enforces thread-safe access. In this case, the variable will be "captured by reference," meaning that the enclosing scope will retain access to the data.

Understanding how the compiler determines whether data can be captured requires a look at Guardian's type system.

Sharing Policy

All types in Guardian have a property called sharing policy. This property describes in which way the type is or isn't thread safe. The sharing policy of a type determines whether the type can be captured by a closure.

There are three sharing policies:

• Value: The type is immutable and has value semantics, meaning that referencing and copying the type are equivalent.
  • Many built-in types, including Fut<T> and all foundation types (int, real, string, bool) are value types.
  • Caveat: Even though instances of a value type are immutable, they may still reside in a mutable binding, such as one created by let mutable. In this case, the variable cannot be captured unless a copy is made.
• Vault: The type has mutable state, but provides thread-safety guarantees. Vault types can always be captured, unless they reside in a mutable binding.
  • The archetypal vault type is GuardVar<T>.
• Unsafe: The type has mutable state and provides no thread-safety guarantees. They can only be captured if they are enclosed in a vault type or are behind a unique reference.

The sharing policy of a type is structurally derived. In other words, the sharing policy of a class or tuple is the most restrictive sharing policy of its members. For example, if you declare a vault class Foo, it may only contain fields of vault or value types, and only in immutable bindings.

The Must-Consume Rule

One of Guardian's concerns is the prevention of the following situations:

• The program terminates too soon because the entry thread didn't wait for all work to finish.
• The program never terminates because no threads make progress towards the termination condition.

In this area, Guardian cannot provide any guarantees, because doing so would require solving the halting problem. However, Guardian does its best to prevent the first situation by enforcing the must-consume rule. This rule stipulates that all Futs generated by an asynchronous operation must eventually be consumed. Imagine a Future as a kind of hot potato: if you receive one, you must either eat it or pass it to somebody else. If you don't do one of these things, the potato's scalding heat will burn your hands.

Here are all the ways to consume a Fut:

• Pass the Fut to a function. The callee, in turn, is subject to the must-consume rule.
• Return the Fut from a function. The caller, in turn, is subject to the must-consume rule.
• Return the Fut from an entry function. This Future, when completed, will cause the program to terminate.
• Adding a continuation to the Fut by calling .then(). This will generate another Fut, which is subject to the must-consume rule.

By itself, this rule would be too restrictive. After all, it's possible for a task that generates a future to make progress by itself in a way that doesn't rely on the future being consumed. For example, if a task signals a latch or performs an async return, those actions advance some other future towards completion, and would therefore render the task's future redundant.

To address this, there is a facet to the must-consume rule called must-consume exemption. These are specific situations that exempt a Fut from the must-consume rule. This exemption can also propagate upwards along a series of nested continuations; the intent here is that any chain of continuations which eventually makes progress in a must-consume-exempt way is itself exempt from the must-consume rule.

Here are all the ways in which a function call can produce a Fut which is exempt from the must-consume rule:

• The function call has a suffix lambda which performs an async return.
  • Rationale: async return implicitly completes a Fut.
• The function call has a suffix lambda which calls signal on a CountdownLatch in all code paths.
  • Rationale: Signaling a latch makes progress towards completing the Fut owned by the latch.
• The function call has a suffix lambda whose final statement has must-consume exemption.
  • This is the method whereby must-consume exemption propagates upwards.
  • Rationale: This indicates that the direct continuation of this task will make progress towards completion.