Merged PR 2844: fix some doc bugs

fix some doc bugs.

Related work items: #2818, #3630, #4374, #4779

docs/_learn/core/specifications.md

@@ -18,14 +18,16 @@ using a `Monitor`.
 Safety property specifications generalize the notion of source code assertions. A safety property
 violation is a finite execution that leads a system to an erroneous state. Coyote provides an API
 for writing assertions that specify safety properties that are local to a Coyote actor or task. In
-the `Task` programming model, you should use `Specification.Assert` and in the `Actor` programming
-model the corresponding API is `Actor.Assert`. In addition, Coyote also provides a way to specify
+the `Task` programming model, you should use `Specification.Assert` (see [Specification
+API](../ref/Microsoft.Coyote.Specifications/SpecificationType)) and in the `Actor` programming model
+the corresponding API is `Actor.Assert`. In addition, Coyote also provides a way to specify
 _global_ assertions that can describe the relationship across tasks or actors.
 
-Coyote provides the notion of a `Monitor`. It is a special kind of actor that can receive events but
-cannot send events to other actors. So it can only observe the execution of a program but not
-influence it: a desirable property when writing specifications in code. A `Monitor` is declared as
-follows:
+Coyote provides the notion of a `Monitor` (see [Monitor
+API](../ref/Microsoft.Coyote.Specifications/MonitorType)). It is a special kind of actor that
+can receive events but cannot send events to other actors. So it can only observe the execution of
+a program but not influence it: a desirable property when writing specifications in code. A
+`Monitor` is declared as follows:
 
 ```c#
 class GlobalSpec : Monitor { ... }

docs/_learn/programming-models/actors/overview.md

@@ -31,6 +31,9 @@ using information you provide declaring how various types of events causes those
 
 See also: [how are Coyote Actors different from existing Microsoft Actor frameworks?](why-actors).
 
+[![image](../../../assets/images/channel9_actors.png)](https://channel9.msdn.com/Shows/On-NET/Reliable-Async-Systems-with-Coyote-Part-2)
+
+
 ### Declaring and creating actors
 
 An actor based program in Coyote is a normal .NET program that also uses the `Actor` or
@@ -272,6 +275,8 @@ e.g. `this.Assert(k == 0)`, which holds if the integer `k` equals to `0`. These
 are useful for local invariants, i.e., they are about the state of a single actor. For global
 invariants it is recommended that you use [Monitors](/coyote/learn/core/specifications).
 
+## Samples
+
 To see a full working example of an `Actor` based program see the [Hello World
 Actors](/coyote/learn/tutorials/hello-world-actors) tutorial.
 

docs/_learn/programming-models/actors/sharing-objects.md

@@ -26,7 +26,7 @@ The following code snippet creates and initializes a `SharedRegister`. It then s
 a different actor `m` by stashing it as part of the payload of an event.
 
 ```c#
-SharedRegister<int> register = SharedRegister.Create<int>(this.Runtime);
+SharedRegister<int> register = SharedRegister.Create<int>(this.Id.Runtime);
 register.SetValue(100);
 this.SendEvent(m, new MyEvent(register, ...));
 var v = register.GetValue();
@@ -70,3 +70,14 @@ intention is to only do read operations on that object).
 
 The same note holds for `SharedRegister<T>` when `T` is a `struct` type with reference fields inside
 it.
+
+## What about System.Collections.Concurrent?
+
+Yes, you can use the .NET thread safe collections to share information across actors but not the
+`BlockingCollection` as this can block and Coyote will not know about that which will lead to
+deadlocks during testing. The other thread safe collections do not have uncontrolled
+non-determinism, either from Task.Run, or from retry loops, timers or waits.
+
+The caveat is that Coyote has not instrumented the .NET concurrent collections, and so coyote does
+not systematically explore thread switching in the middle of these operations, therefore Coyote
+will not always find all data race conditions related to concurrent access on these collections.

docs/_learn/programming-models/async/overview.md

@@ -30,6 +30,8 @@ between controlled `Task` objects. In production, a controlled `Task` executes e
 simple wrapper over a native `Task`, with operations being pass-through (Coyote takes control only
 during testing).
 
+[![image](../../../assets/images/channel9_tasks.png)](https://channel9.msdn.com/Shows/On-NET/Reliable-Async-Systems-with-Coyote-Part-1)
+
 ## Overview
 
 The core of the Coyote asynchronous tasks programming model is the controlled `Task` and `Task<T>`
@@ -94,51 +96,63 @@ Say that you have the following simple C# program:
 using Microsoft.Coyote.Tasks;
 using Microsoft.Coyote.Specifications;
 
-public class SharedEntry
+public class Program
 {
     public int Value = 0;
-}
 
-public async Task WriteWithDelayAsync(SharedEntry entry, int value)
-{
-    await Task.Delay(100);
-    entry.Value = value;
-}
+  public async Task WriteWithDelayAsync(int value)
+  {
+      await Task.Delay(100);
+      this.Value = value;
+  }
 
-public async Task RunAsync()
-{
-    SharedEntry entry = new SharedEntry();
+  public async Task RunAsync()
+  {
+      Task task1 = WriteWithDelayAsync(3);
+      Task task2 = WriteWithDelayAsync(5);
 
-    Task task1 = WriteWithDelayAsync(entry, 3);
-    Task task2 = WriteWithDelayAsync(entry, 5);
+      await Task.WhenAll(task1, task2);
 
-    await Task.WhenAll(task1, task2);
-
-    Specification.Assert(entry.Value == 5, "Value is '{0}' instead of 5.", entry.Value);
+      Specification.Assert(this.Value == 5, "Value is '{0}' instead of 5.", this.Value);
+  }
 }
 ```
 
-The above program contains a `SharedEntry` type that implements a shared container for an `int`
-value. The `WriteWithDelayAsync` is a C# `async` method that asynchronously waits for a controlled
-`Task` to complete after `100`ms (created via the `Task.Delay(100)` call), and then modifies the
-value of the `SharedEntry` object.
+The above program contains a `int Value` that is updated by the `WriteWithDelayAsync` method. This
+is a C# `async` method that asynchronously waits for a controlled `Task` to complete after `100`ms
+(created via the `Task.Delay(100)` call), and then modifies the Value field.
 
-The `RunAsync` asynchronous method is creating a new `SharedEntry` object, and then twice invokes
-the `WriteWithDelayAsync` method by passing the values `3` and `5` respectively. Each method call
-returns a controlled `Task` object, which can be awaited using `await`. The `RunAsync` method first
-invokes the two asynchronous method calls and then calls `Task.WhenAll(...)` to `await` on the
-completion of both tasks.
+The asynchronous `RunAsync` method twice invokes the `WriteWithDelayAsync` method by passing the
+values `3` and `5` respectively. Each method call returns a controlled `Task` object, which can be
+awaited using `await`. The `RunAsync` method first invokes the two asynchronous method calls and
+then calls `Task.WhenAll(...)` to `await` on the completion of both tasks.
 
-Because `WriteWithDelayAsync` method awaits a `Task.Delay` to complete, it will yield control to the
-caller of the method, which is the `RunAsync` method. However, the `RunAsync` method is not awaiting
-immediately upon invoking the `WriteWithDelayAsync` method calls. This means that the two calls can
-happen _asynchronously_, and thus the value in the `SharedEntry` object can be either `3` or `5`
-after `Task.WhenAll(...)` completes.
+Because `WriteWithDelayAsync` method awaits a `Task.Delay` to complete, it will yield control to
+the caller of the method, which is the `RunAsync` method. However, the `RunAsync` method is not
+awaiting immediately upon invoking the `WriteWithDelayAsync` method calls. This means that the two
+calls can happen _asynchronously_, and thus the resulting Value can be either `3` or `5` after
+`Task.WhenAll(...)` completes.
 
 Using `Specification.Assert`, Coyote allows you to write assertions that check these kinds of safety
-properties. In this case, the assertion will check if the value is `5` or not, and if not it will
+properties. In this case, the assertion will check if the Value is `5` or not, and if not it will
 throw an exception, or report an error together with a reproducible trace during testing.
 
+## What about System.Collections.Concurrent?
+
+Yes, you can use the .NET thread safe collections to share information across tasks, but not the
+`BlockingCollection` as this can block and Coyote will not know about that which will lead to
+deadlocks during testing. The other thread safe collections do not have uncontrolled
+non-determinism, either from Task.Run, or from retry loops, timers or waits.
+
+The caveat is that Coyote has not instrumented the .NET concurrent collections, and so coyote does
+not systematically explore thread switching in the middle of these operations, therefore Coyote
+will not always find all data race conditions related to concurrent access on these collections.
+For example, two tasks calling `TryAdd` with the same key, one task will succeed the other will
+not, but Coyote will not systematically explore all possible orderings around this operation. You
+can help Coyote do better by using [ExploreContextSwitch](interleavings).
+
+## Samples
+
 To try out more samples built using the _asynchronous tasks_ programming model see the following:
 
 - [Hello world tasks](/coyote/learn/tutorials/hello-world-tasks)

docs/_learn/programming-models/async/synchronized-block.md

@@ -80,5 +80,8 @@ Bugs involving `System.Threading.Monitor` can be extremely tricky to debug due t
 and can given you clear 100% reproducible bug schedules that you can replay as slowly as you need
 to see what is really going on leading up to such bugs.
 
-For a complete example see the [BoundedBuffer
-sample](https://github.com/microsoft/coyote-samples/tree/master/BoundedBuffer).
+## Sample
+
+For a complete example see the [Extreme Programming meets systematic testing using
+Coyote](https://cloudblogs.microsoft.com/opensource/2020/07/14/extreme-programming-meets-systematic-testing-using-coyote/)
+and the associated [BoundedBuffer example source code](https://github.com/microsoft/coyote-samples/tree/master/BoundedBuffer).