if("${CMAKE_SYSTEM}" MATCHES "Linux")
foreach(x
-# barber_shop_deadlock producer_consumer_deadlock
+#
# simple_cond_broadcast_deadlock simple_semaphore_deadlock simple_barrier_deadlock simple_cond_deadlock
# simple_semaphores_deadlock
-# philosophers_mutex_deadlock
-# philosophers_semaphores_deadlock
+#
+#
# philosophers_spurious_deadlock
# simple_barrier_with_threads_deadlock
# simple_semaphores_with_threads_deadlock
# simple_mutex_deadlock
# simple_mutex_with_threads_deadlock
- barber_shop_ok
-# philosophers_mutex_ok philosophers_semaphores_ok
-# producer_consumer_ok producer_consumer_spurious_nok
+ barber_shop_ok barber_shop_deadlock
+ philosophers_semaphores_ok philosophers_semaphores_deadlock
+ philosophers_mutex_ok philosophers_mutex_deadlock
+ producer_consumer_ok producer_consumer_deadlock
+
+
+ # producer_consumer_spurious_nok # infinite no-op loop
+
+#
+#
# simple_barrier_ok simple_barrier_with_threads_ok simple_cond_broadcast_ok
# simple_cond_broadcast_with_semaphore_ok simple_cond_ok simple_mutex_ok
# simple_mutex_with_threads_ok simple_semaphores_ok simple_semaphores_with_threads_ok simple_threads_ok
--- /dev/null
+#define _REENTRANT
+
+#include <stdio.h>
+#include <unistd.h>
+#include <stdlib.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+// The maximum number of customer threads.
+#define MAX_CUSTOMERS 10
+
+// Define the semaphores.
+sem_t waitingRoom;
+sem_t barberChair;
+sem_t barberPillow;
+sem_t seatBelt;
+
+// Flag to stop the barber thread when all customers have been serviced.
+int allDone = 0;
+int DEBUG = 0;
+
+static void *customer(void *number) {
+ int num = *(int *)number;
+
+ if(DEBUG) printf("Customer %d leaving for barber shop.\n", num);
+ if(DEBUG) printf("Customer %d arrived at barber shop.\n", num);
+
+ sem_wait(&waitingRoom);
+
+ if(DEBUG) printf("Customer %d entering waiting room.\n", num);
+
+ sem_wait(&barberChair);
+
+ if(DEBUG) printf("Customer %d waking the barber.\n", num);
+ sem_post(&barberPillow);
+
+ sem_wait(&seatBelt);
+
+ sem_post(&barberChair);
+ if(DEBUG) printf("Customer %d leaving barber shop.\n", num);
+ return NULL;
+}
+
+static void *barber(void *junk) {
+ while (!allDone) {
+ if(DEBUG) printf("The barber is sleeping\n");
+ sem_wait(&barberPillow);
+
+ if (!allDone) {
+ if(DEBUG) printf("The barber is cutting hair\n");
+ if(DEBUG) printf("The barber has finished cutting hair.\n");
+ sem_post(&seatBelt);
+ }
+ else {
+ if(DEBUG) printf("The barber is going home for the day.\n");
+ }
+ }
+ return NULL;
+}
+
+int main(int argc, char *argv[]) {
+ if(argc != 5){
+ printf("Usage: %s numCustomers numChairs RandSeed DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ pthread_t btid;
+ pthread_t tid[MAX_CUSTOMERS];
+ int i, numCustomers, numChairs;
+ long RandSeed;
+ int Number[MAX_CUSTOMERS];
+
+ numCustomers = atoi(argv[1]);
+ numChairs = atoi(argv[2]);
+ RandSeed = atol(argv[3]);
+ DEBUG = atoi(argv[4]);
+
+ if (numCustomers > MAX_CUSTOMERS) {
+ printf("The maximum number of Customers is %d.\n", MAX_CUSTOMERS);
+ exit(-1);
+ }
+
+ srand48(RandSeed);
+
+ for (i=0; i<MAX_CUSTOMERS; i++) {
+ Number[i] = i;
+ }
+
+ sem_init(&waitingRoom, 0, numChairs);
+ sem_init(&barberChair, 0, 1);
+ sem_init(&barberPillow, 0, 0);
+ sem_init(&seatBelt, 0, 0);
+
+ pthread_create(&btid, NULL, barber, NULL);
+
+ for (i=0; i<numCustomers; i++) {
+ pthread_create(&tid[i], NULL, customer, (void *)&Number[i]);
+ }
+
+ for (i=0; i<numCustomers; i++) {
+ pthread_join(tid[i],NULL);
+ }
+
+ allDone = 1;
+ sem_post(&barberPillow);
+ pthread_join(btid,NULL);
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+! expect return 3
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-barber_shop_deadlock 5 3 0 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something.
+> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
+> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:6)
+> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:2 not granted)
+> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted)
+> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 1, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 3, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 3, no timeout)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 1, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 3, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 4, no timeout)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 1, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 2, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 2)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_ASYNC_LOCK(semaphore: 3)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_WAIT(semaphore: 3, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorJoin(target 5, no timeout)
+> [0.000000] [mc_global/INFO] Actor 6 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 7 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3;3;3;3;3;2;2;2;3;3;3;1;4;4;4;4;4;2;2;2;4;4;4;1;5;5;5;5;5;2;2;2;5;5;5;1;6;7'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 40 unique states visited; 0 backtracks (0 transition replays, 40 states visited overall)
\ No newline at end of file
--- /dev/null
+// Naive dining philosophers solution, which leads to deadlock.
+
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <stdlib.h>
+
+int DEBUG = 0;
+
+struct forks {
+ int philosopher;
+ pthread_mutex_t *left_fork;
+ pthread_mutex_t *right_fork;
+} *forks;
+
+static void * philosopher_doit(void *forks_arg) {
+ struct forks *forks = forks_arg;
+ pthread_mutex_lock(forks->left_fork);
+ pthread_mutex_lock(forks->right_fork);
+
+ if(DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher);
+
+ pthread_mutex_unlock(forks->left_fork);
+ pthread_mutex_unlock(forks->right_fork);
+ return NULL;
+}
+
+int main(int argc, char* argv[]) {
+ if(argc != 3){
+ printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ int NUM_THREADS = atoi(argv[1]);
+ DEBUG = atoi(argv[2]);
+
+ pthread_t thread[NUM_THREADS];
+ pthread_mutex_t mutex_resource[NUM_THREADS];
+
+ forks = malloc(NUM_THREADS * sizeof(struct forks));
+
+ int i;
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_mutex_init(&mutex_resource[i], NULL);
+ forks[i] = (struct forks){i,
+ &mutex_resource[i], &mutex_resource[(i+1) % NUM_THREADS]};
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]);
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_join(thread[i], NULL);
+ }
+
+ free(forks);
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+! expect return 3
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_mutex_deadlock 5 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 6 actors are still running, waiting for something.
+> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
+> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2)
+> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3)
+> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4)
+> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:3 owner:5)
+> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:4 owner:6)
+> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 3, owner: 5)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_WAIT(mutex: 3, owner: 5)
+> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 4, owner: 6)
+> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_WAIT(mutex: 4, owner: 6)
+> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;4;3;4;5;4;5;6;5;6;6'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1298 unique states visited; 199 backtracks (3432 transition replays, 4929 states visited overall)
\ No newline at end of file
--- /dev/null
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <stdlib.h>
+
+int DEBUG = 0;
+
+struct forks {
+ int philosopher;
+ pthread_mutex_t *left_fork;
+ pthread_mutex_t *right_fork;
+ pthread_mutex_t *dining_fork;
+};
+
+static void * philosopher_doit(void *forks_arg) {
+ struct forks *forks = forks_arg;
+ pthread_mutex_lock(forks->dining_fork);
+ pthread_mutex_lock(forks->left_fork);
+ pthread_mutex_lock(forks->right_fork);
+ pthread_mutex_unlock(forks->dining_fork);
+
+ if(DEBUG)
+ printf("Philosopher %d is eating.\n", forks->philosopher);
+
+ pthread_mutex_unlock(forks->left_fork);
+ pthread_mutex_unlock(forks->right_fork);
+ return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+ if(argc != 3){
+ printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ int NUM_THREADS = atoi(argv[1]);
+ DEBUG = atoi(argv[2]);
+
+ pthread_t thread[NUM_THREADS];
+ pthread_mutex_t mutex_resource[NUM_THREADS];
+ struct forks forks[NUM_THREADS];
+
+ pthread_mutex_t dining_fork;
+ pthread_mutex_init(&dining_fork, NULL);
+
+ int i;
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_mutex_init(&mutex_resource[i], NULL);
+ forks[i] = (struct forks){i,
+ &mutex_resource[i],
+ &mutex_resource[(i+1) % NUM_THREADS],
+ &dining_fork};
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]);
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_join(thread[i], NULL);
+ }
+
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_mutex_ok 5 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14170 unique states visited; 2087 backtracks (45202 transition replays, 61459 states visited overall)
\ No newline at end of file
--- /dev/null
+// Dining philosophers solution with semaphores
+
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+
+struct forks {
+ int philosopher;
+ pthread_mutex_t *left_fork;
+ pthread_mutex_t *right_fork;
+ sem_t* sem_dining;
+ int DEBUG;
+} *forks;
+
+static void * philosopher_doit(void *forks_arg) {
+ struct forks *forks = forks_arg;
+ sem_wait(forks->sem_dining);
+ pthread_mutex_lock(forks->left_fork);
+ pthread_mutex_lock(forks->right_fork);
+
+ if(forks->DEBUG) printf("Philosopher %d just ate.\n", forks->philosopher);
+
+ pthread_mutex_unlock(forks->left_fork);
+ pthread_mutex_unlock(forks->right_fork);
+ sem_post(forks->sem_dining);
+ return NULL;
+}
+
+int main(int argc, char* argv[]) {
+ if(argc != 3){
+ printf("Usage: %s NUM_PHILOSOPHERS DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ int NUM_THREADS = atoi(argv[1]);
+ int DEBUG = atoi(argv[2]);
+
+ pthread_t thread[NUM_THREADS];
+ pthread_mutex_t mutex_resource[NUM_THREADS];
+ sem_t sem_dining;
+ sem_init(&sem_dining, 0, NUM_THREADS);
+
+ forks = malloc(NUM_THREADS * sizeof(struct forks));
+
+ int i;
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_mutex_init(&mutex_resource[i], NULL);
+ forks[i] = (struct forks){i,
+ &mutex_resource[i],
+ &mutex_resource[(i+1) % NUM_THREADS],
+ &sem_dining,
+ DEBUG};
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]);
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_join(thread[i], NULL);
+ }
+
+ free(forks);
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+! expect return 3
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_deadlock 3 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 4 actors are still running, waiting for something.
+> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
+> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2)
+> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3)
+> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:2 owner:4)
+> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_WAIT(mutex: 2, owner: 4)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;3;3;3;2;3;4;4;4;3;4;4'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 890 unique states visited; 90 backtracks (1415 transition replays, 2395 states visited overall)
--- /dev/null
+#include <stdio.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <semaphore.h>
+#include <stdlib.h>
+
+int DEBUG = 0;
+
+struct forks {
+ int philosopher;
+ pthread_mutex_t *left_fork;
+ pthread_mutex_t *right_fork;
+ sem_t* sem_dining;
+};
+
+static void * philosopher_doit(void *forks_arg) {
+ struct forks *forks = forks_arg;
+ sem_wait(forks->sem_dining);
+ pthread_mutex_lock(forks->left_fork);
+ pthread_mutex_lock(forks->right_fork);
+
+ if(DEBUG)
+ printf("Philosopher %d is eating.\n", forks->philosopher);
+
+ pthread_mutex_unlock(forks->left_fork);
+ pthread_mutex_unlock(forks->right_fork);
+ sem_post(forks->sem_dining);
+ return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+ if(argc != 3){
+ printf("Usage: %s NUM_THREADS DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ int NUM_THREADS = atoi(argv[1]);
+ DEBUG = atoi(argv[2]);
+
+ pthread_t thread[NUM_THREADS];
+ pthread_mutex_t mutex_resource[NUM_THREADS];
+ struct forks forks[NUM_THREADS];
+
+ sem_t sem_dining;
+ sem_init(&sem_dining, 0, NUM_THREADS - 1);
+
+ int i;
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_mutex_init(&mutex_resource[i], NULL);
+ forks[i] = (struct forks){i,
+ &mutex_resource[i],
+ &mutex_resource[(i+1) % NUM_THREADS],
+ &sem_dining};
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_create(&thread[i], NULL, &philosopher_doit, &forks[i]);
+ }
+
+ for (i = 0; i < NUM_THREADS; i++) {
+ pthread_join(thread[i], NULL);
+ }
+
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-philosophers_semaphores_ok 3 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 2268 unique states visited; 233 backtracks (3314 transition replays, 5815 states visited overall)
\ No newline at end of file
--- /dev/null
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+int MaxItems; // Maximum items a producer can produce or a consumer can consume
+int BufferSize; // Size of the buffer
+
+sem_t empty;
+sem_t full;
+int in = 0;
+int out = 0;
+int *buffer;
+pthread_mutex_t mutex;
+
+int DEBUG = 0; // Debug flag
+
+static void *producer(void *pno)
+{
+ int item;
+ for(int i = 0; i < MaxItems; i++) {
+ item = rand(); // Produce a random item
+ pthread_mutex_lock(&mutex);
+ sem_wait(&empty);
+ buffer[in] = item;
+ if(DEBUG) printf("Producer %d: Insert Item %d at %d\n", *((int *)pno),buffer[in],in);
+ in = (in+1)%BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&full);
+ }
+ return NULL;
+}
+
+static void *consumer(void *cno)
+{
+ for(int i = 0; i < MaxItems; i++) {
+ pthread_mutex_lock(&mutex);
+ sem_wait(&full);
+ int item = buffer[out];
+ if(DEBUG) printf("Consumer %d: Remove Item %d from %d\n",*((int *)cno),item, out);
+ out = (out+1)%BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&empty);
+ }
+ return NULL;
+}
+
+int main(int argc, char* argv[]) {
+ if(argc != 4){
+ printf("Usage: %s MAX_ITEMS BUFFER_SIZE DEBUG\n", argv[0]);
+ return 1;
+ }
+
+ MaxItems = atoi(argv[1]);
+ BufferSize = atoi(argv[2]);
+ DEBUG = atoi(argv[3]);
+
+ buffer = (int*) malloc(BufferSize * sizeof(int));
+
+ pthread_t pro[5],con[5];
+ pthread_mutex_init(&mutex, NULL);
+ sem_init(&empty,0,BufferSize);
+ sem_init(&full,0,0);
+
+ int a[5] = {1,2,3,4,5}; //Just used for numbering the producer and consumer
+
+ for(int i = 0; i < 5; i++) {
+ pthread_create(&pro[i], NULL, producer, (void *)&a[i]);
+ }
+ for(int i = 0; i < 5; i++) {
+ pthread_create(&con[i], NULL, consumer, (void *)&a[i]);
+ }
+
+ for(int i = 0; i < 5; i++) {
+ pthread_join(pro[i], NULL);
+ }
+ for(int i = 0; i < 5; i++) {
+ pthread_join(con[i], NULL);
+ }
+
+ free(buffer);
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+! expect return 3
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-producer_consumer_deadlock 5 3 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 11 actors are still running, waiting for something.
+> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
+> [0.000000] [ker_engine/INFO] Actor 1 (main thread@Lilibeth) simcall ActorJoin(pid:2)
+> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall SEM_WAIT(sem_id:0 not granted)
+> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 4 (thread 3@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 5 (thread 4@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 6 (thread 5@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 7 (thread 6@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 8 (thread 7@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 9 (thread 8@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 10 (thread 9@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [ker_engine/INFO] Actor 11 (thread 10@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_WAIT(semaphore: 0, granted: yes)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_UNLOCK(mutex: 0, owner: -1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_UNLOCK(semaphore: 1)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall SEM_ASYNC_LOCK(semaphore: 0)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 4 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 5 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 6 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 7 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 8 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 9 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 10 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 11 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;3;4;5;6;7;8;9;10;11'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 31 unique states visited; 0 backtracks (0 transition replays, 31 states visited overall)
--- /dev/null
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <pthread.h>
+#include <semaphore.h>
+
+#define MaxBufferSize 5
+
+sem_t empty;
+sem_t full;
+int in = 0;
+int out = 0;
+int buffer[MaxBufferSize];
+pthread_mutex_t mutex;
+int BufferSize;
+int ItemCount;
+int DEBUG;
+
+static void *producer(void *pno)
+{
+ int item;
+ for(int i = 0; i < ItemCount; i++) {
+ item = rand(); // Produce an random item
+ sem_wait(&empty);
+ pthread_mutex_lock(&mutex);
+ buffer[in] = item;
+ if (DEBUG) {
+ printf("Producer %d: Insert Item %d at %d\n",
+ *((int *)pno),buffer[in],in);
+ }
+ in = (in+1)%BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&full);
+ }
+ return NULL;
+}
+
+static void *consumer(void *cno)
+{
+ for(int i = 0; i < ItemCount; i++) {
+ sem_wait(&full);
+ pthread_mutex_lock(&mutex);
+ int item = buffer[out];
+ if (DEBUG) {
+ printf("Consumer %d: Remove Item %d from %d\n",
+ *((int *)cno),item, out);
+ }
+ out = (out+1)%BufferSize;
+ pthread_mutex_unlock(&mutex);
+ sem_post(&empty);
+ }
+ return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+ if (argc < 6) {
+ printf("Usage: %s <NUM_PRODUCERS> <NUM_CONSUMERS> <ITEM_COUNT> <BUFFER_SIZE> <DEBUG>\n", argv[0]);
+ return 1;
+ }
+
+ int NUM_PRODUCERS = atoi(argv[1]);
+ int NUM_CONSUMERS = atoi(argv[2]);
+ ItemCount = atoi(argv[3]);
+ BufferSize = atoi(argv[4]);
+ DEBUG = atoi(argv[5]);
+
+ pthread_t pro[NUM_PRODUCERS],con[NUM_CONSUMERS];
+
+ pthread_mutex_init(&mutex, NULL);
+ sem_init(&empty,0,BufferSize);
+ sem_init(&full,0,0);
+
+ int a[NUM_PRODUCERS > NUM_CONSUMERS ? NUM_PRODUCERS : NUM_CONSUMERS];
+
+ for(int i = 0; i < NUM_PRODUCERS; i++) {
+ a[i] = i+1;
+ pthread_create(&pro[i], NULL, producer, (void *)&a[i]);
+ }
+ for(int i = 0; i < NUM_CONSUMERS; i++) {
+ a[i] = i+1;
+ pthread_create(&con[i], NULL, consumer, (void *)&a[i]);
+ }
+
+ for(int i = 0; i < NUM_PRODUCERS; i++) {
+ pthread_join(pro[i], NULL);
+ }
+ for(int i = 0; i < NUM_CONSUMERS; i++) {
+ pthread_join(con[i], NULL);
+ }
+
+ return 0;
+}
--- /dev/null
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/mcmini/mcmini-producer_consumer_ok 2 2 2 1 0
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1953 unique states visited; 491 backtracks (12324 transition replays, 14768 states visited overall)
\ No newline at end of file
