Support for rewriting SemaphoreSlim?

[camerondm9]

I'm attempting to use Coyote to check for bugs in a library of mine, but some of my code is using System.Threading.SemaphoreSlim, which currently isn't supported.
It seems that there is a compatible implementation already available here:
https://github.com/microsoft/coyote/blob/main/Source/Core/Tasks/Locks/Semaphore.cs
My code seems to work normally when I manually rewrite it to use this implementation.

Could a rewrite rule be added to directly support code which uses SemaphoreSlim, or is there a detail I've missed?

[pdeligia]

Thanks for trying out Coyote @camerondm9, and raising this issue! No you are right, if you manually switch to the Semaphore implementation available in Coyote then it will indeed work, it is just that we did not add yet a rewriting pass to automate this type.

We basically used to ask developers to manually change the default .NET types to the "concurrency testable" versions provided by Coyote, like this Semaphore one, but a few months ago we introduced rewriting to fully automate this process and make it much more user friendly. So far we have focused on the most common TPL types, but we are happy to add rewriting for SemaphoreSlim, as its already there after all :)

I will ping you once I add it to rewriting. Btw, we also welcome (and would love) contributions if tackling this was something that you would be interested to try out! Feel free to let me know in that case.

[pdeligia]

Closing as this is duplicate of #368, this is now supported and will be available in the next release.

[jhwj9617]

@pdeligia
Hey Pantazis. Its great we support semaphoreslim now, but is it recommended at all the use when authoring mocks? Or is it better to use regular lock statements. I figure it would be more accurate "simulator" when using regular locks.

[pdeligia]

Hey Joon (@jhwj9617), the main benefit of using SemaphoreSlim right now is that it's implemented in a more optimal way than regular lock statements, mostly because it does not need to worry about reentrancy that the lock statement provides (I need to get back to optimize that soon). I think if you want a simple exclusive lock and don't care about reentrancy, then right now new SemaphoreSlim(1,1) will most likely give you better mileage!

Btw, working on 1.7.1 (will come out in the next few days) that will optimize SemaphoreSlim even more (there is a rare memory leak that is happening right now, although mostly affects cases where someone uses the --max-steps N flag).