Await guarantees

Consider the following simple program:

```lang-cs
using System;
using System.Threading.Tasks;

int a = 1;
await Task.Yield();
Console.WriteLine(a);
```

I'm trying to prove (based on the standard) that the output will be exactly 1 and not e. g. 0 due to threading issues.

The parts of the code on the different sides of `await` can run in different threads, so there is no guarantee of data dependence preservation through the first bullet in [§8.10 Execution order](https://github.com/dotnet/csharpstandard/blob/draft-v6/standard/basic-concepts.md#810-execution-order).

There is no explicit synchronization (`lock`, etc.), no threads are started (the second thread is a thread pool thread), no volatile fields are explicitly accessed, so nothing from the third bullet seems to be directly applicable.

It's clear that the synchronization must be done in some form, perhaps by `ThreadPool.QueueUserWorkItem`, but I couldn't find anything in the standard which _guarantees_ this behavior.

I assume that the guarantees like these are very basic and must be listed in the standard and not forward to the concrete implementation details or CLR specs.