Safer asynchronous workflows for GUI programming

In the previous article, I discussed how to use F# asynchronous work­flows for creating reactive user-interfaces. One of the main concerns was to avoid blocking the GUI thread (to prevent the user-interface from freezing). The workflow shouldn't perform any CPU-intensive compu­tation when running on the GUI thread.

The standard F# library provides two ways to run a computation on a background thread from an asynchronous workflow. The StartChild operation starts an operation in the thread pool and returns a workflow that can be called using asynchronous (non-blocking) let! construct. The SwitchToThreadPool operation can be called using do! and resumes the rest of the workflow on a background thread.

When using the SwitchToThreadPool operation, we also need to eventually use SwitchToContext to transfer the execution back to the GUI thread (after completing the CPU-intensive calculations). In this article, I describe a variation of F# asynchronous workflows that keeps track of the running thread in the type of the computation. As a result, calling a workflow that should be executed on a GUI thread from a background thread is a compile-time error as opposed to failing at runtime.

Introducing checked async

The easiest way to implement checked asynchronous workflows is to just wrap the standard F# implementation and add type parameters for keeping the additional information. Then we also need to create a wrapper for a computation builder that will correctly propagate the additional information. Let's first look at the type declarations and then explore some examples. The definition of computation builder is briefly discussed at the end of the article.

1: /// Represents an asynchronous computation that starts
2: /// on the 'Pre thread, ends on the 'Post thread and
3: /// produces a value of type 'Value.
4: type CheckedAsync<'Pre, 'Post, 'Value> = (...)
5: 
6: // Two phantom types to represent threads
7: type GuiThread = (...)
8: type BackgroundThread = (...)

The last type parameter of CheckedAsync is the type of the value produced by the asynchronous workflow and is uses as an argument to the wrapped Async. The two additional parameters are called phantom type parameters, because they do not appear anywhere in the definition. In many ways, they are similar to units of measure - they just add additional information to the type that is checked at compile-time.

The next two types can be used in place of the first two type parameters. For example, a computation of type CheckedAsync<GuiThread, BackgroundThread, string> represents an asynchronous computation that starts on the GUI thread (where it can access user-interface elements), then switches to the background thread (which can be done using SwitchToThreadPool), then performs some CPU-intensive computation and produces a string value. When called using let! from another asynchronous workflow, it resumes the rest of the workflow on the background thread (which is quite subtle behavior - most of the standard asynchronous operations resume on the same thread where they started).

Processing data and creating charts

To demonstrate how checked asynchronous workflows work in practice, we'll reimplement the examples from my previous article. The sample application downloads stock prices, processes them (which may be CPU consuming) and then creates a chart (which must be run on the GUI thread). The following two helper functions will be called from the main asynchronous workflow:

 1: /// Parse downloaded data set. This is a CPU-expensive 
 2: /// computation that should not block the user-interface.
 3: let extractStockPrices (data:string) count = asyncOn background {
 4:   let dataLines = (...)
 5:   let data = (...)
 6:   // Additional CPU-bound data processing
 7:   Thread.Sleep(5000)
 8:   return data }
 9: 
10: /// Create & display chart. The function needs to 
11: /// access user interface and should run on GUI thread.
12: let displayChart color prices = asyncOn gui {
13:   let chart = createChart 600.0 200.0 color prices
14:   chart.SetValue(Canvas.LeftProperty, 100.0)
15:   chart.SetValue(Canvas.TopProperty, 100.0)
16:   holder.Children.Clear()
17:   holder.Children.Add(chart) }

The functions are declared almost like ordinary asynchronous workflow. The only difference is that the snippet uses a parameterized computation builder asyncOn. The argument specifies the thread where the computation should start (the values gui and background are just dummy values to specify the type using a nice syntax). The F# compiler infers the thread where the computation will complete from the initial thread and from the code of the workflow. Both of the functions are quite simple and they do not change the thread where the workflow is running. As a result the type of the first workflow is CheckedAsync<BackgroundThread, BackgroundThread, float[]> and the type of the second one is CheckedAsync<GuiThread, GuiThread, unit>.

Type-checking threads

The main workflow needs to call the above two functions. When it gets the data, it processes them to extract the prices (and possibly other statistics) and then draws the chart. Let's now look how could we go about writing a composed workflow. In this case, we don't need to be explicit about the thread where the computation starts. To leave the compiler to infer this, we can use asyncChecked computation builder instead of more specific asyncOn. In the first attempt we just try to call the two functions:

1: let wrongWorkflow data = asyncChecked {
2:   // Starts executing on background thread...
3:   let! prices = extractStockPrices data 500
4:   // ...but cannot continue on the GUI thread!
5:   do! displayChart Color.Red prices }

As the snippet shows, the code doesn't compile. The problem is that the workflow created by extractStockPrices ends on the background thread, but the workflow created by displayChart can be only started on the GUI thread. The definition of Bind in the computation builder (discussed below) specifies that the end-thread of the first operation must match the begin-thread of the second operation, which is not the case in this snippet. Also note that the F# type inference correctly deduced that the entire wrongWorkflow starts on the background thread, because this is where the first operation starts. This also follows from the definition of the computation builder.

To fix the error, we need to run the workflow created by displayChart on the GUI thread. One way to do this is to use a special operation named SwitchToGui that changes the current thread to the GUI thread using the Dispatcher type provided by Silverlight. The method has the following type:

1: type CheckedAsync with
2:   /// Continue executing on the GUI thread (regardless of the current thread)
3:   static member SwitchToGui : unit -> CheckedAsync<'Pre, GuiThread, unit>

The type of the workflow specifies that it can be started on any thread. The type parameter 'Pre can be specified to both GuiThread (which would be legal, but not very useful) and to BackgroundThread. The resulting thread is however always GuiThread. Finally, the last type parameter specifies that the workflow returns unit, which means that it can be called using the do! syntax:

1: let goodWorkflow data = asyncChecked {
2:   // Start executing on background thread
3:   let! prices = extractStockPrices data 500
4:   // Switch to the GUI thread
5:   do! CheckedAsync.SwitchToGui()
6:   // And display chart on the GUI thread
7:   do! displayChart Color.Red prices }

With the additional thread transition in the middle, the snippet now type-checks and it creates a workflow that starts on the background thread, does some work, switches to the GUI thread and then displays the chart and returns. You can verify that by looking at the (inferred) type of the goodWorkflow function.

Verifying stock price sample

Let's now look how checked asynchronous workflows work on a larger example. First of all, the previous article included an incorrect example that called the two functions declared above from a single asynchronous workflow without any thread switching. The example compiled, but it caused the user-interface to hang, which is what we want to avoid. The main workflow is expected to start on the GUI thread. If we replace ordinary async with asyncOn gui and use operations provided by CheckedAsync (instead of Async), the snippet no longer compiles:

 1: let main = asyncOn gui {
 2:     (Initialization omitted)
 3:   
 4:   // The main application loop
 5:   while true do 
 6:     // Wait until the user selects stock (GUI operation)
 7:     let! color, stock = CheckedAsync.AwaitObservable(stockClicked)
 8:     // Download data for stock (non-blocking operation)
 9:     let wc = new WebClient()
10:     let! data = wc.AsyncDownloadString(Uri(root + stock))    
11:     // Process data (CPU-bound operation)
12:     let! prices = extractStockPrices data 500
13:     // Create & display the chart (GUI operation)
14:     do! displayChart color prices }
15: 
16: // Start the workflow immediately (on GUI thread)
17: do main |> CheckedAsync.StartImmediate

The error is the same as in the earlier brief example - we cannot call CPU-bound workflow extractStockPrices from a workflow that runs on the GUI thread. When writing code using checked workflows, we need to use checked versions of all standard operations. These are implemented as simple wrappers, but they annotate the type with the specification of threading behavior (which is otherwise difficult to find, even in the documentation). The operations used in the above example have the following signatures:

 1: type CheckedAsync with
 2:   /// Waiting for event occurrence is allowed on GUI thread only
 3:   static member AwaitObservable  : IObservable<'T> -> 
 4:                                    CheckedAsync<GuiThread, GuiThread, 'T>
 5:   /// Starts a computation on the (current) GUI thread
 6:   static member StartImmediate   : CheckedAsync<GuiThread, 'Post, unit> 
 7: 
 8: type System.Net.WebClient with
 9:   /// Downloads string and returns to original thread
10:   member AsyncDownloadString : Uri -> CheckedAsync<'T, 'T, string>

The types of operations now also carry the specification of threading behavior.

• The AwaitObservable operation can be used only on the GUI thread and it resumes the workflow on the GUI thread. This works for standard F# events, but other sources of IObservable<'T> may behave differently (the right solution would be to use a more expressive type IObservable<'Thread, 'T> with 'Thread describing where events are triggered).
• The StartImmediate operation starts a workflow on the current thread. It is expected to be used on the main thread (outside of asynchronous workflows), so the type specifies that the argument will be executed on the GUI thread. The operation doesn't care where the workflow completes, so it uses a type variable 'Post.
• The AsyncDownloadString operation is implemented such that it returns back to the original thread where it was started. This is behavior used by most of the standard F# asynchronous operations and is captured by the fact that the same type variable ('T) is used for both starting and finishing thread.

Now that we've seen numerous primitive asynchronous operations, let's look how to fix the above example. The following two sections implement the two approaches introduced in the previous article. We start with switching of the current thread and then look at starting computation as a child.

Switching between threads

After introducing the type-checking of threading behavior, the switching approach makes more sense. In the earlier snippet, I demonstrated how the SwitchToGui operation makes that possible, but that's a Silverlight-specific operation. In general, F# asynchronous workflows use standard .NET SynchronizationContext type that represents an arbitrary thread (it can be either background or GUI). Current context can be obtained using Synchronization­Context.­Current. The following snippet uses checked wrappers for these operations:

 1: let main = asyncOn gui {
 2:   (Initialization omitted)
 3: 
 4:   // The main application loop
 5:   while true do 
 6:     // Wait until the user selects stock (GUI operation)
 7:     let! color, stock = CheckedAsync.AwaitObservable(stockClicked)
 8:     // Download data for stock (non-blocking operation)
 9:     let wc = new WebClient()
10:     let! data = wc.AsyncDownloadString(Uri(root + stock))    
11: 
12:     // Process data (CPU-bound operation)
13:     let! ctx = CheckedAsync.CurrentContext()
14:     do! CheckedAsync.SwitchToThreadPool()
15:     let! prices = extractStockPrices data 500
16:     do! CheckedAsync.SwitchToContext(ctx)
17: 
18:     // Create & display the chart (GUI operation)
19:     do! displayChart color prices }

Before we can call the extractStockPrices function, we need to switch the execution of the workflow to a back­ground thread. This is done simply using SwitchToThreadPool which resumes the workflow on a thread from the thread pool. To switch back, we use SwitchToContext, which resumes the workflow on a thread represented by the SynchronizationContext used as an argument. This may be either a GUI or a background thread - to make this type-safe, we need to keep track of the thread in the type of synchronization context too, so we use a wrapper Synchronization­Context<'Thread>. The type parameter 'Thread represents the thread captured by the context.

When getting the current context, we use an operation CurrentContextprovided by CheckedAsync. It returns a synchronization context of the current thread and annotates it with an appropriate type. When executed from a workflow running on a thread SomeThread, the result will have a type Synchronization­Context<SomeThread>. The type signatures of the operation used in the above snippet clarify the behavior:

 1: type CheckedAsync with
 2:   /// Get current context (the thread is also kept in the type)
 3:   static member CurrentContext :
 4:     unit -> CheckedAsync<'T, 'T, SynchronizationContext<'T>>
 5:   /// Switch to new background thread (from any thread)
 6:   static member SwitchToThreadPool :
 7:     unit -> CheckedAsync<'T, BackgroundThread, unit>
 8:   /// Switch to thread represented by a synchronization context
 9:   static member SwitchToContext : 
10:     SynchronizationContext<'T> -> CheckedAsync<'Pre, 'T, unit>

The CurrentContext method creates a workflow that starts on a thread 'T, ends on a thread 'T and returns a synchronization context representing the same thread 'T. When used in the snippet above, the operation is called from the GUI thread and so the type of ctx is Synchronization­Context<GuiThread>. The SwitchToContext operation takes a typed synchronization context representing a thread 'T and creates an asynchronous workflow that resumes on a thread specified by the context. In the above example, the operation switches the execution to a GUI thread (stored previously), so that we can call the displayChart function.

The use of generic types when working with synchronization contexts demonstrated one of the fascinating things about programming in F# that is carried over to checking of threads in asynchronous workflows. We can easily write polymorphic code that works with any values and executes on any threads while still checking that computations are composed correctly. With a bit of effort, it is even possible to capture dynamic behavior introduced by synchro­nization contexts.

Starting child workflow

Another way to run a computation without blocking the GUI thread is to start it as a child workflow. This is done using the StartChild operation that guarantees that it will not introduce blocking. When using this approach, it is almost impossible to write the code in a wrong way, so there is less need for thread checking. However, when we annotate the operation, it has an interesting type that is worth demonstrating:

 1: let main = asyncOn gui {
 2:   (Initialization omitted)
 3: 
 4:   // The main application loop
 5:   while true do 
 6:     // Wait until the user selects stock (GUI operation)
 7:     let! color, stock = CheckedAsync.AwaitObservable(stockClicked)
 8:     // Download data for stock (non-blocking operation)
 9:     let wc = new WebClient()
10:     let! data = wc.AsyncDownloadString(Uri(root + stock))    
11:     
12:     // Process data (CPU-bound operation)
13:     let! token = CheckedAsync.StartChild(extractStockPrices data 500)
14:     let! prices = token
15: 
16:     // Create & display the chart (GUI operation)
17:     do! displayChart color prices }

The StartChild operation creates a workflow that can be executed on any thread (and finishes on the same thread). We immediately execute it using the let! construct. This starts the workflow given as an argument on the background thread (which is also specified by the type of the argument). The result is a token that can be used for waiting for the completion of the background operation. This operation can be (again) used on any thread, because it performs non-blocking waiting. The whole type signature looks as follows:

1: type CheckedAsync with
2:   /// Start child on a background thread (without changing current thread)
3:   static member StartChild : 
4:     CheckedAsync<BackgroundThread, 'Post, 'R> ->
5:     CheckedAsync<'Pre1, 'Pre1, CheckedAsync<'Pre2, 'Pre2, 'R>>

As already explained, the argument should be a workflow that can be started on the background thread and we don't care where it completes. The result of the operation is a checked asynchronous workflow (that waits for the completion) wrapped in another checked asynchronous operation (that starts the task). These two operations use two different type parameters to track the thread, because it is perfectly possible to use them from different threads. For example, we may start the background operation on a GUI thread and then pass the result to some other workflow that will wait on another background thread (in which case 'Pre1 would be GuiThread and 'Pre2 would be BackgroundThread).

Looking under the cover

The key idea of the approach demonstrated in this article is to extend the type of asynchronous workflows to also include two type parameters that do not appear in the type definition (these are called phantom types). The additional type parameters specify threads where the workflow starts and where it completes. Then we need to annotate standard async operations with the additional types to specify the behavior. I demonstrated type signatures of several of the operations of the CheckedAsync type earlier in the article. The implementation can be found in the source code, but is mostly trivial - just wrap the operation from standard F# async and add types.

The last important piece is to specify how the operations compose. When you run one operation and then some other operation, the resulting thread of the first one must match the starting thread of the second one. This rule is also used by the F# compiler to infer the types of operations written using asyncChecked and to infer the type of operations that can be run on any thread and preserve the thread (such as AsyncDownloadString).

The composition rules are defined by the F# computation builder. The following snippet shows the type signatures of the standard operations and also adds While (which was used in the example and is quite interesting too):

 1: type CheckedAsyncBuilder =
 2:   /// Return creates async workflow that resumes on the same thread
 3:   member Return : 'V -> CheckedAsync<'Thread, 'Thread, 'V>
 4:   /// Composed computation starts on 'Pre, switches to 'Interm and
 5:   /// then switches to 'Post (The result hides the intermediate step)
 6:   member Bind   : CheckedAsync<'Pre, 'Interm, 'V1> -> 
 7:                   ('V1 -> CheckedAsync<'Interm, 'Post, 'V2>) ->
 8:                   CheckedAsync<'Pre, 'Post, 'V2>
 9:   /// The body of a while loop must end at the same thread as where it 
10:   /// was started (otherwise it cannot be composed to run multiple times)
11:   member While  : (unit -> bool) -> CheckedAsync<'Thread, 'Thread, unit> ->
12:                   CheckedAsync<'Thread, 'Thread, unit>

If we consider just the last type parameter (representing the value returned by a checked asynchronous workflow), the types are the standard types of a monad (and an F# computation builder). However, the first two type parameters add an interesting additional power:

• The Return operation creates an asynchronous workflow that immediately returns the given value. It doesn't interact with threads in any way - the workflow will finish on the same thread where it was started.
• The Bind operation is interesting. It takes a workflow of type CheckedAsync<'Pre, 'Interm, 'V1> as the first argument. In order to produce the result, it needs to evaluate this workflow first. This means that the computation will start on the 'Pre thread and end on the 'Interm thread. Then the operator calls the provided function and gets a workflow of type CheckedAsync<'Interm, 'Post, 'V2>. This workflow can be executed after the first one because the ending thread of the first one matches the starting thread of the second. After executing, the result will be reported on the thread 'Post, so the overall computation starts on 'Pre and ends on 'Post (which is reflected by the returned workflow type).
• The snippet also shows the type of While, which takes a function that is called to test whether a condition holds and the (asynchronous) body. When the loop executes the body repeatedly, the body must end at the same thread where it started. This directly follows from the type of Bind and the way Bind can be used to implement While. The typing rule for the For operation would be similar.

Another interesting operation that is not discussed in detail in this article is TryWith, which represents an exception handler. This is quite tricky, because the exception will be handled on the thread where it happened, but that can be any thread where the body of the workflow can run!

In the source code, I solved this problem by adding a new type named AnyThread, which is not compatible with any other type. For practical purposes, this is probably sufficient, but you can imagine several possible extensions. The AnyThread type could be a base type of both GuiThread and BackgroundThread making it possible to compose computations that end on a specific thread with a computation that starts on any (unknown) thread. We could also use even more complicated types in to track all possible threads that can be used by the body and then have types like AnyOf<GuiThread, BackgroundThread> representing any of the two. However, this doesn't add much practical value and it may be only interesting from a research perspective.

Some of the ideas that I mentioned above have been actually done in different contexts. Although this is a blog post and not a research paper, the next section mentions several of the related academic papers (as well as some readable blog posts). If you're interested only in practical uses of checked asynchronous workflows, then you can safely skip it.

Related work

The definition of a monad used in this article adds two type parameters to capture the required initial state (a pre-condition) and a resulting state (a post-condition). This idea is quite common when reasoning about programming languages and it can be traced back to Hoare logic [1]. In Hoare logic, the pre- and post-conditions are not written as part of the progam - they are just a way of reasoning about existing programs. More recent work on "Hoare type theory" tries to embed this reasoning in the types of programs.

More specifically, the signature of monadic operations that I used in the previous section is also called parameterized monad and has been studied from the theoretical perspective [2], but there is also a more readable introduction [3]. It can be used for a variety of other things (besides threads in asynchronous workflows), such as tracking of acative file handles [4].

Summary

In this article, I demonstrated an extension of F# asynchronous workflows that makes them safer. It adds a way to track where the workflow is executing - whether it is a GUI thread or a background thread. We can create computations that should be executed on the background thread using asyncOn background. These can safely perform long-running CPU-intensive computations and we know that this won't freeze the user-interface. Similarly, we can create workflows that can be only executed on the GUI thread using asyncOn gui. These computations can safely access user-interface elements.

Thanks to the right definition of a computation builder, the current thread is automatically tracked in the asynchronous workflow syntax. Calling a workflow that should run on a particular thread from a wrong thread is a compile-time error. This adds very useful additional checking. The examples in this article relied on some help from the programmer. We had to explicitly mark extractStockPrices as background-thread computaiton and displayChart as GUI-thread computation. In a perfect world, the compiler would know that certain operations should be executed only on certain threads and it would infer the type for us...

Downloads & Source code

• Browse the source code on GitHub
• Download the source code (ZIP)

References 

• [1] Hoare logic - Wikipedia
• [2] Parameterised Notions of Computations - Robert Atkey
• [3] Beyond Monads - A Neighborhood of Infinity
• [4] Lightweight monadic regions - Oleg Kiselyov, Chung-chieh Shan