adding support for rewriting concurrent bags (#209)

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

@@ -0,0 +1,123 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Runtime.CompilerServices;
+
+namespace Microsoft.Coyote.Interception
+{
+    /// <summary>
+    /// Provides methods for controlling <see cref="ConcurrentBag{T}"/> 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 ControlledConcurrentBag
+    {
+        /// <summary>
+        /// Gets the number of elements contained in the <see cref="ConcurrentBag{T}"/>.
+        /// </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<T>(ConcurrentBag<T> concurrentBag)
+#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
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.Count;
+        }
+
+        /// <summary>
+        /// Gets a value that indicates whether the <see cref="ConcurrentBag{T}"/> 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<T>(ConcurrentBag<T> concurrentBag)
+#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
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.IsEmpty;
+        }
+
+        /// <summary>
+        /// Adds an object to the <see cref="ConcurrentBag{T}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static void Add<T>(ConcurrentBag<T> concurrentBag, T item)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            concurrentBag.Add(item);
+        }
+
+#if !NETSTANDARD2_0 && !NETFRAMEWORK
+        /// <summary>
+        /// Removes all objects from the <see cref="ConcurrentBag{T}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static void Clear<T>(ConcurrentBag<T> concurrentBag)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            concurrentBag.Clear();
+        }
+#endif
+
+        /// <summary>
+        /// Copies the <see cref="ConcurrentBag{T}"/> elements to an existing one-dimensional <see cref="Array"/>,
+        /// starting at the specified array index.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static void CopyTo<T>(ConcurrentBag<T> concurrentBag, T[] array, int index)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            concurrentBag.CopyTo(array, index);
+        }
+
+        /// <summary>
+        /// Returns an enumerator that iterates through the  <see cref="ConcurrentBag{T}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static IEnumerator<T> GetEnumerator<T>(ConcurrentBag<T> concurrentBag)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.GetEnumerator();
+        }
+
+        /// <summary>
+        /// Copies the elements stored in the <see cref="ConcurrentBag{T}"/> to a new <see cref="Array"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static T[] ToArray<T>(ConcurrentBag<T> concurrentBag)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.ToArray();
+        }
+
+        /// <summary>
+        /// Tries to return an object from the beginning of the <see cref="ConcurrentBag{T}"/> without removing it.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryPeek<T>(ConcurrentBag<T> concurrentBag, out T result)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.TryPeek(out result);
+        }
+
+        /// <summary>
+        /// Attempts to remove and return an object from the <see cref="ConcurrentBag{T}"/>.
+        /// </summary>
+        [MethodImpl(MethodImplOptions.AggressiveInlining)]
+        public static bool TryTake<T>(ConcurrentBag<T> concurrentBag, out T result)
+        {
+            ConcurrentCollectionHelper.Interleave();
+            return concurrentBag.TryTake(out result);
+        }
+    }
+}

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

@@ -9,7 +9,7 @@ using System.Runtime.CompilerServices;
 namespace Microsoft.Coyote.Interception
 {
     /// <summary>
-    /// Provides methods for creating concurrent dictionaries that can be controlled during testing.
+    /// Provides methods for controlling <see cref="ConcurrentDictionary{TKey, TValue}"/> 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)]

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

@@ -9,7 +9,7 @@ using System.Runtime.CompilerServices;
 namespace Microsoft.Coyote.Interception
 {
     /// <summary>
-    /// Provides methods for creating concurrent queues that can be controlled during testing.
+    /// Provides methods for controlling <see cref="ConcurrentQueue{T}"/> 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)]

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

@@ -9,7 +9,7 @@ using System.Runtime.CompilerServices;
 namespace Microsoft.Coyote.Interception
 {
     /// <summary>
-    /// Static implementation of the Properties and Methods of <see cref="ConcurrentStack{T}"/> that coyote uses for testing.
+    /// Provides methods for controlling <see cref="ConcurrentStack{T}"/> 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)]

Source/Test/Rewriting/CachedNameProvider.cs

@@ -50,6 +50,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 ConcurrentBagFullName { get; } = typeof(SystemConcurrentCollections.ConcurrentBag<>).FullName;
         internal static string ConcurrentDictonaryFullName { get; } = typeof(SystemConcurrentCollections.ConcurrentDictionary<,>).FullName;
         internal static string ConcurrentQueueFullName { get; } = typeof(SystemConcurrentCollections.ConcurrentQueue<>).FullName;
         internal static string ConcurrentStackFullName { get; } = typeof(SystemConcurrentCollections.ConcurrentStack<>).FullName;

Source/Test/Rewriting/Passes/ConcurrentCollectionRewriter.cs

@@ -85,7 +85,11 @@ namespace Microsoft.Coyote.Rewriting
             if (type is GenericInstanceType genericType)
             {
                 string fullName = genericType.ElementType.FullName;
-                if (fullName == CachedNameProvider.ConcurrentDictonaryFullName)
+                if (fullName == CachedNameProvider.ConcurrentBagFullName)
+                {
+                    type = this.Module.ImportReference(typeof(ControlledConcurrentBag));
+                }
+                else if (fullName == CachedNameProvider.ConcurrentDictonaryFullName)
                 {
                     type = this.Module.ImportReference(typeof(ControlledConcurrentDictionary));
                 }

Tests/Tests.BugFinding/ConcurrencyFuzzing/Collections/ConcurrentBagTests.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 ConcurrentBagTests : Tests.ConcurrentCollections.ConcurrentBagTests
+    {
+        public ConcurrentBagTests(ITestOutputHelper output)
+                : base(output)
+        {
+        }
+
+        private protected override SchedulingPolicy SchedulingPolicy => SchedulingPolicy.Fuzzing;
+
+        protected override Configuration GetConfiguration()
+        {
+            return base.GetConfiguration().WithConcurrencyFuzzingEnabled();
+        }
+    }
+}

Tests/Tests.BugFinding/ConcurrentCollections/ConcurrentBagTests.cs

@@ -0,0 +1,94 @@
+// 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 ConcurrentBagTests : BaseBugFindingTest
+    {
+        public ConcurrentBagTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentBagProperties()
+        {
+            this.Test(() =>
+            {
+                var concurrentBag = new ConcurrentBag<int>();
+                Assert.True(concurrentBag.IsEmpty);
+
+                concurrentBag.Add(1);
+                var count = concurrentBag.Count;
+                Assert.Equal(1, count);
+                Assert.Single(concurrentBag);
+
+#if !NETSTANDARD2_0 && !NETFRAMEWORK
+                concurrentBag.Clear();
+                Assert.Empty(concurrentBag);
+#endif
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentBagMethods()
+        {
+            this.Test(() =>
+            {
+                var concurrentBag = new ConcurrentBag<int>();
+                Assert.True(concurrentBag.IsEmpty);
+
+                concurrentBag.Add(1);
+                Assert.Single(concurrentBag);
+
+                bool peekResult = concurrentBag.TryPeek(out int peek);
+                Assert.True(peekResult);
+                Assert.Equal(1, peek);
+
+                int[] expectedArray = { 1 };
+                var actualArray = concurrentBag.ToArray();
+                Assert.Equal(expectedArray, actualArray);
+
+                bool takeResult = concurrentBag.TryTake(out int _);
+                Assert.True(takeResult);
+                Assert.Empty(concurrentBag);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestConcurrentBagMethodsWithRaceCondition()
+        {
+            this.TestWithError(() =>
+            {
+                var concurrentBag = new ConcurrentBag<int>();
+
+                var t1 = Task.Run(() =>
+                {
+                    concurrentBag.Add(1);
+                    concurrentBag.Add(2);
+
+                    Specification.Assert(concurrentBag.Count == 2, "Value is {0} instead of 2.", concurrentBag.Count);
+                });
+
+                var t2 = Task.Run(() =>
+                {
+                    concurrentBag.TryTake(out int _);
+                });
+
+                Task.WaitAll(t1, t2);
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(100),
+            expectedError: "Value is 1 instead of 2.",
+            replay: true);
+        }
+    }
+}

Tests/Tests.BugFinding/ConcurrentCollections/ConcurrentQueueTests.cs

@@ -59,9 +59,9 @@ namespace Microsoft.Coyote.BugFinding.Tests.ConcurrentCollections
                 Assert.Equal(2, concurrentQueue.Count);
                 Assert.Equal(expectedArray, actualArray);
 
-                bool dequeueResult = concurrentQueue.TryDequeue(out int dequeue);
+                bool dequeueResult = concurrentQueue.TryDequeue(out int dequeueValue);
                 Assert.True(dequeueResult);
-                Assert.Equal(1, dequeue);
+                Assert.Equal(1, dequeueValue);
                 Assert.Single(concurrentQueue);
 
 #if !NETSTANDARD2_0 && !NETFRAMEWORK