Now that lincheck property supports suspending functions please add test for linearizability of Semaphore and Mutex