adding support for rewriting concurrent dictionaries (#202)

Source/Core/Interception/Collections/Concurrent/ControlledConcurrentDictionary.cs

@@ -0,0 +1,297 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Runtime.CompilerServices;
+using Microsoft.Coyote.Runtime;
+
+namespace Microsoft.Coyote.Interception
+{
+    /// <summary>
+    /// Provides methods for creating concurrent dictionaries that can be controlled during testing.
+    /// </summary>
+    /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
+    [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+    public static class ControlledConcurrentDictionary
+    {
+        /// <summary>
+        /// Gets the number of key/value pairs contained in the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        public static int get_Count<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            return concurrentDictionary.Count;
+        }
+
+        /// <summary>
+        /// Gets a value that indicates whether the <see cref="ConcurrentDictionary{TKey, TValue}"/> is empty.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        public static bool get_IsEmpty<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            return concurrentDictionary.IsEmpty;
+        }
+
+        /// <summary>
+        /// Gets the value associated with the specified key.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        public static TValue get_Item<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            return concurrentDictionary[key];
+        }
+
+        /// <summary>
+        /// Sets the value associated with the specified key.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        public static void set_Item<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, TValue value)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            concurrentDictionary[key] = value;
+        }
+
+        /// <summary>
+        /// Gets a collection containing the keys in the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static ICollection<TKey> get_Keys<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            return concurrentDictionary.Keys;
+        }
+
+        /// <summary>
+        /// Gets a collection containing the values in the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+#pragma warning disable CA1707 // Identifiers should not contain underscores
+#pragma warning disable SA1300 // Element should begin with upper-case letter
+#pragma warning disable IDE1006 // Naming Styles
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static ICollection<TValue> get_Values<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+#pragma warning restore IDE1006 // Naming Styles
+#pragma warning restore SA1300 // Element should begin with upper-case letter
+#pragma warning restore CA1707 // Identifiers should not contain underscores
+        {
+            Interleave();
+            return concurrentDictionary.Values;
+        }
+
+        private static void Interleave()
+        {
+            var runtime = CoyoteRuntime.Current;
+            if (runtime.SchedulingPolicy is SchedulingPolicy.Systematic)
+            {
+                runtime.ScheduleNextOperation(AsyncOperationType.Default);
+            }
+            else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)
+            {
+                runtime.DelayOperation();
+            }
+        }
+
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not
+        /// already exist, or updates a key/value pair in the <see cref="ConcurrentDictionary{TKey, TValue}"/>
+        /// if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue AddOrUpdate<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, Func<TKey, TValue> addValueFactory,
+            Func<TKey, TValue, TValue> updateValueFactory)
+        {
+            Interleave();
+            return concurrentDictionary.AddOrUpdate(key, addValueFactory, updateValueFactory);
+        }
+
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not
+        /// already exist, or updates a key/value pair in the <see cref="ConcurrentDictionary{TKey, TValue}"/>
+        /// if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue AddOrUpdate<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, TValue addValue,
+            Func<TKey, TValue, TValue> updateValueFactory)
+        {
+            Interleave();
+            return concurrentDictionary.AddOrUpdate(key, addValue, updateValueFactory);
+        }
+
+#if !NETSTANDARD2_0 && !NETFRAMEWORK
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not
+        /// already exist, or updates a key/value pair in the <see cref="ConcurrentDictionary{TKey, TValue}"/>
+        /// if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue AddOrUpdate<TKey, TArg, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, Func<TKey, TArg, TValue> addValueFactory,
+            Func<TKey, TValue, TArg, TValue> updateValueFactory, TArg factoryArgument)
+        {
+            Interleave();
+            return concurrentDictionary.AddOrUpdate(key, addValueFactory, updateValueFactory, factoryArgument);
+        }
+#endif
+
+        /// <summary>
+        /// Removes all keys and values from the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static void Clear<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+        {
+            Interleave();
+            concurrentDictionary.Clear();
+        }
+
+        /// <summary>
+        /// Determines whether the <see cref="ConcurrentDictionary{TKey, TValue}"/> contains the specified key.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool ContainsKey<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key)
+        {
+            Interleave();
+            return concurrentDictionary.ContainsKey(key);
+        }
+
+        /// <summary>
+        /// Returns an enumerator that iterates through the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+        {
+            Interleave();
+            return concurrentDictionary.GetEnumerator();
+        }
+
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not already exist.
+        /// Returns the new value, or the existing value if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue GetOrAdd<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, Func<TKey, TValue> valueFactory)
+        {
+            Interleave();
+            return concurrentDictionary.GetOrAdd(key, valueFactory);
+        }
+
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not already exist.
+        /// Returns the new value, or the existing value if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue GetOrAdd<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, TValue value)
+        {
+            Interleave();
+            return concurrentDictionary.GetOrAdd(key, value);
+        }
+
+#if !NETSTANDARD2_0 && !NETFRAMEWORK
+        /// <summary>
+        /// Adds a key/value pair to the <see cref="ConcurrentDictionary{TKey, TValue}"/> if the key does not already exist.
+        /// Returns the new value, or the existing value if the key already exists.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static TValue GetOrAdd<TKey, TArg, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, Func<TKey, TArg, TValue> valueFactory,
+            TArg factoryArgument)
+        {
+            Interleave();
+            return concurrentDictionary.GetOrAdd(key, valueFactory, factoryArgument);
+        }
+#endif
+
+        /// <summary>
+        /// Copies the key and value pairs stored in the <see cref="ConcurrentDictionary{TKey, TValue}"/> to a new array.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static KeyValuePair<TKey, TValue>[] ToArray<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary)
+        {
+            Interleave();
+            return concurrentDictionary.ToArray();
+        }
+
+        /// <summary>
+        /// Attempts to add the specified key and value to the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryAdd<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, TValue value)
+        {
+            Interleave();
+            return concurrentDictionary.TryAdd(key, value);
+        }
+
+        /// <summary>
+        /// Attempts to get the value associated with the specified key from the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryGetValue<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, out TValue value)
+        {
+            Interleave();
+            return concurrentDictionary.TryGetValue(key, out value);
+        }
+
+        /// <summary>
+        /// Attempts to remove and return the value that has the specified key from the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryRemove<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, out TValue value)
+        {
+            Interleave();
+            return concurrentDictionary.TryRemove(key, out value);
+        }
+
+#if !NETSTANDARD2_1 && !NETSTANDARD2_0 && !NETFRAMEWORK
+        /// <summary>
+        /// Attempts to remove and return the value that has the specified key from the <see cref="ConcurrentDictionary{TKey, TValue}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryRemove<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, KeyValuePair<TKey, TValue> item)
+        {
+            Interleave();
+            return concurrentDictionary.TryRemove(item);
+        }
+#endif
+
+        /// <summary>
+        /// Updates the value associated with key to newValue if the existing value with key is equal to comparisonValue.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryUpdate<TKey, TValue>(ConcurrentDictionary<TKey, TValue> concurrentDictionary, TKey key, TValue newValue, TValue comparisonValue)
+        {
+            Interleave();
+            return concurrentDictionary.TryUpdate(key, newValue, comparisonValue);
+        }
+    }
+}

Source/Core/Interception/Collections/Generic/ControlledDictionary.cs

@@ -327,12 +327,12 @@ namespace Microsoft.Coyote.Interception
         private class Mock<TKey, TValue> : Dictionary<TKey, TValue>
         {
             /// <summary>
-            /// Count of read accesses to the list.
+            /// Count of read accesses to the dictionary.
             /// </summary>
             private volatile int ReaderCount;
 
             /// <summary>
-            /// Count of write accesses to the list.
+            /// Count of write accesses to the dictionary.
             /// </summary>
             private volatile int WriterCount;
 

Source/Test/Rewriting/CachedNameProvider.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using SystemCompiler = System.Runtime.CompilerServices;
+using SystemConcurrentCollections = System.Collections.Concurrent;
 using SystemGenericCollections = System.Collections.Generic;
 using SystemTasks = System.Threading.Tasks;
 using SystemThreading = System.Threading;
@@ -48,5 +49,7 @@ namespace Microsoft.Coyote.Rewriting
 
         internal static string GenericListFullName { get; } = typeof(SystemGenericCollections.List<>).FullName;
         internal static string GenericDictionaryFullName { get; } = typeof(SystemGenericCollections.Dictionary<,>).FullName;
+
+        internal static string ConcurrentDictonaryFullName { get; } = typeof(SystemConcurrentCollections.ConcurrentDictionary<,>).FullName;
     }
 }

Source/Test/Rewriting/Passes/ConcurrentCollectionRewriter.cs

@@ -0,0 +1,97 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Interception;
+using Microsoft.Coyote.IO;
+using Mono.Cecil;
+using Mono.Cecil.Cil;
+
+namespace Microsoft.Coyote.Rewriting
+{
+    /// <summary>
+    /// Rewrites the concurrent collection types to their controlled versions to enable Coyote explore interleavings during testing.
+    /// </summary>
+    internal class ConcurrentCollectionRewriter : AssemblyRewriter
+    {
+        /// <summary>
+        /// Initializes a new instance of the <see cref="ConcurrentCollectionRewriter"/> class.
+        /// </summary>
+        internal ConcurrentCollectionRewriter(ILogger logger)
+            : base(logger)
+        {
+        }
+
+        /// <inheritdoc/>
+        internal override void VisitMethod(MethodDefinition method)
+        {
+            this.Method = null;
+
+            // Only non-abstract method bodies can be rewritten.
+            if (!method.IsAbstract)
+            {
+                this.Method = method;
+                this.Processor = method.Body.GetILProcessor();
+
+                // Rewrite the method body instructions.
+                this.VisitInstructions(method);
+            }
+        }
+
+        /// <inheritdoc/>
+        protected override Instruction VisitInstruction(Instruction instruction)
+        {
+            if (this.Method is null)
+            {
+                return instruction;
+            }
+
+            if ((instruction.OpCode == OpCodes.Call || instruction.OpCode == OpCodes.Callvirt) &&
+                instruction.Operand is MethodReference methodReference)
+            {
+                instruction = this.VisitCallInstruction(instruction, methodReference);
+            }
+
+            return instruction;
+        }
+
+        /// <summary>
+        /// Rewrites the specified non-generic <see cref="OpCodes.Call"/> or <see cref="OpCodes.Callvirt"/> instruction.
+        /// </summary>
+        /// <returns>The unmodified instruction, or the newly replaced instruction.</returns>
+        private Instruction VisitCallInstruction(Instruction instruction, MethodReference method)
+        {
+            MethodReference newMethod = this.RewriteMethodReference(method, this.Module);
+            if (method.FullName == newMethod.FullName || !this.TryResolve(newMethod, out MethodDefinition _))
+            {
+                // There is nothing to rewrite, return the original instruction.
+                return instruction;
+            }
+
+            // Create and return the new instruction.
+            Instruction newInstruction = Instruction.Create(OpCodes.Call, newMethod);
+            newInstruction.Offset = instruction.Offset;
+
+            Debug.WriteLine($"............. [-] {instruction}");
+            this.Replace(instruction, newInstruction);
+            Debug.WriteLine($"............. [+] {newInstruction}");
+
+            return newInstruction;
+        }
+
+        /// <inheritdoc/>
+        protected override TypeReference RewriteDeclaringTypeReference(MethodReference method)
+        {
+            TypeReference type = method.DeclaringType;
+            if (type is GenericInstanceType genericType)
+            {
+                string fullName = genericType.ElementType.FullName;
+                if (fullName == CachedNameProvider.ConcurrentDictonaryFullName)
+                {
+                    type = this.Module.ImportReference(typeof(ControlledConcurrentDictionary));
+                }
+            }
+
+            return type;
+        }
+    }
+}

Source/Test/Rewriting/RewritingEngine.cs

@@ -129,6 +129,7 @@ namespace Microsoft.Coyote.Rewriting
             {
                 new TaskRewriter(this.Logger),
                 new MonitorRewriter(this.Logger),
+                new ConcurrentCollectionRewriter(this.Logger),
                 new ExceptionFilterRewriter(this.Logger)
             };
 

Tests/Tests.BugFinding/ConcurrencyFuzzing/Collections/ConcurrentDictionaryTests.cs

@@ -0,0 +1,23 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Runtime;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.BugFinding.Tests.ConcurrencyFuzzing
+{
+    public class ConcurrentDictionaryTests : Tests.ConcurrentCollections.ConcurrentDictionaryTests
+    {
+        public ConcurrentDictionaryTests(ITestOutputHelper output)
+                : base(output)
+        {
+        }
+
+        private protected override SchedulingPolicy SchedulingPolicy => SchedulingPolicy.Fuzzing;
+
+        protected override Configuration GetConfiguration()
+        {
+            return base.GetConfiguration().WithConcurrencyFuzzingEnabled();
+        }
+    }
+}

Tests/Tests.BugFinding/ConcurrentCollections/ConcurrentDictionaryTests.cs

@@ -0,0 +1,164 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Concurrent;
+using System.Threading.Tasks;
+using Microsoft.Coyote.Specifications;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.BugFinding.Tests.ConcurrentCollections
+{
+    public class ConcurrentDictionaryTests : BaseBugFindingTest
+    {
+        public ConcurrentDictionaryTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentDictionaryProperties()
+        {
+            this.Test(() =>
+            {
+                var concurrentDictionary = new ConcurrentDictionary<int, bool>();
+                Assert.True(concurrentDictionary.IsEmpty);
+
+                concurrentDictionary[0] = false;
+                Assert.True(concurrentDictionary[0] == false);
+                Assert.Single(concurrentDictionary);
+
+                concurrentDictionary.Clear();
+                Assert.Empty(concurrentDictionary);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentDictionaryMethodsSubsetOne()
+        {
+            this.Test(() =>
+            {
+                var concurrentDictionary = new ConcurrentDictionary<int, int>();
+                Assert.True(concurrentDictionary.IsEmpty);
+
+                int value = concurrentDictionary.GetOrAdd(1, (key) => 1);
+                Assert.Equal(1, value);
+                Assert.True(concurrentDictionary.ContainsKey(1));
+                Assert.Single(concurrentDictionary);
+
+                concurrentDictionary.AddOrUpdate(1, 1, (key, oldValue) => oldValue * 10);
+                Assert.True(concurrentDictionary[1] == 10);
+                Assert.True(concurrentDictionary.ContainsKey(1));
+                Assert.Single(concurrentDictionary);
+
+                value = concurrentDictionary.GetOrAdd(1, 100);
+                Assert.Equal(10, value);
+                Assert.True(concurrentDictionary.ContainsKey(1));
+                Assert.Single(concurrentDictionary);
+
+                concurrentDictionary.AddOrUpdate(2, (key) => 2, (key, oldValue) => oldValue * 10);
+                Assert.True(concurrentDictionary[2] == 2);
+                Assert.True(concurrentDictionary.Count == 2);
+                Assert.True(concurrentDictionary.ContainsKey(1));
+                Assert.True(concurrentDictionary.ContainsKey(2));
+
+                concurrentDictionary.TryUpdate(2, 20, 2);
+                Assert.True(concurrentDictionary[2] == 20);
+                Assert.True(concurrentDictionary.Count == 2);
+
+                concurrentDictionary.Clear();
+                Assert.Empty(concurrentDictionary);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentDictionaryMethodsSubsetOneWithRaceCondition()
+        {
+            this.TestWithError(() =>
+            {
+                var concurrentDictionary = new ConcurrentDictionary<int, int>();
+
+                var t1 = Task.Run(() =>
+                {
+                    var value1 = concurrentDictionary.AddOrUpdate(1, 1, (key, oldValue) => oldValue * 10);
+                    var value2 = concurrentDictionary.GetOrAdd(1, 2);
+
+                    Specification.Assert(value1 == value2, "Value is {0} instead of {1}.", value2, value1);
+                });
+
+                var t2 = Task.Run(() =>
+                {
+                    concurrentDictionary.AddOrUpdate(1, 2, (key, oldValue) => 2);
+                });
+
+                Task.WaitAll(t1, t2);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100),
+            expectedError: "Value is 2 instead of 1.",
+            replay: true);
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentDictionaryMethodsSubsetTwo()
+        {
+            this.Test(() =>
+            {
+                var concurrentDictionary = new ConcurrentDictionary<int, int>();
+                Assert.True(concurrentDictionary.IsEmpty);
+
+                bool result = concurrentDictionary.TryAdd(1, 1);
+                Assert.True(result);
+                Assert.True(concurrentDictionary.ContainsKey(1));
+                Assert.Single(concurrentDictionary);
+
+                result = concurrentDictionary.TryGetValue(1, out int value);
+                Assert.True(result);
+                Assert.Equal(1, value);
+
+                result = concurrentDictionary.TryUpdate(1, 10, 1);
+                Assert.True(result);
+                Assert.True(concurrentDictionary[1] == 10);
+
+                concurrentDictionary.TryRemove(1, out value);
+                Assert.Empty(concurrentDictionary);
+                Assert.Equal(10, value);
+
+                result = concurrentDictionary.TryGetValue(1, out value);
+                Assert.False(result);
+
+                concurrentDictionary.Clear();
+                Assert.Empty(concurrentDictionary);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentDictionaryMethodsSubsetTwoWithRaceCondition()
+        {
+            this.TestWithError(() =>
+            {
+                var concurrentDictionary = new ConcurrentDictionary<int, bool>();
+
+                var t1 = Task.Run(() =>
+                {
+                    concurrentDictionary.TryAdd(1, true);
+                    var count = concurrentDictionary.Count;
+                    Specification.Assert(count is 1, "Count is {0} instead of 1.", count);
+                });
+
+                var t2 = Task.Run(() =>
+                {
+                    concurrentDictionary.Clear();
+                });
+
+                Task.WaitAll(t1, t2);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100),
+            expectedError: "Count is 0 instead of 1.",
+            replay: true);
+        }
+    }
+}

Tools/Coyote/Program.cs

@@ -75,8 +75,7 @@ namespace Microsoft.Coyote
                 Console.WriteLine("Microsoft (R) Coyote version {0} for .NET{1}",
                     typeof(CommandLineOptions).Assembly.GetName().Version,
                     GetDotNetVersion());
-                Console.WriteLine("Copyright (C) Microsoft Corporation. All rights reserved.");
-                Console.WriteLine();
+                Console.WriteLine("Copyright (C) Microsoft Corporation. All rights reserved.\n");
             }
 
             SetEnvironment(configuration);