From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Sun, 26 Feb 2023 16:17:19 +0000 (+0100)
Subject: Allow to control the problem size from the cmd line, and reduce the instance in MC
X-Git-Tag: v3.34~432
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b060880e24efd3d1862694ab007a8b98c42adcc7

Allow to control the problem size from the cmd line, and reduce the instance in MC

The previous instance size resulted in a timeout now that the DPOR
reduction is less efficient (because it's less buggy)
---

diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh
index c2714170ea..0766ba31f7 100644
--- a/examples/sthread/pthread-mc-producer-consumer.tesh
+++ b/examples/sthread/pthread-mc-producer-consumer.tesh
@@ -1,7 +1,8 @@
 # We ignore the LD_PRELOAD lines from the expected output because they contain the build path
 ! ignore .*LD_PRELOAD.*
 
-$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q
+$ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -c 2 -C 1 -p 2 -P 1
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
 > [0.000000] [sthread/INFO] Starting the simulation.
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1819 unique states visited; 108 backtracks (6808 transition replays, 4882 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 719 unique states visited; 83 backtracks (1854 transition replays, 1053 states visited overall)
diff --git a/examples/sthread/pthread-producer-consumer.c b/examples/sthread/pthread-producer-consumer.c
index 8fd1a0b16b..cf69840fd8 100644
--- a/examples/sthread/pthread-producer-consumer.c
+++ b/examples/sthread/pthread-producer-consumer.c
@@ -10,18 +10,19 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
+#include <unistd.h>
 
-#define AmountProduced 3 /* Amount of items produced by a producer */
-#define AmountConsumed 3 /* Amount of items consumed by a consumer */
-#define ProducerCount 2  /* Amount of producer threads*/
-#define ConsumerCount 2  /* Amount of consumer threads*/
-#define BufferSize 4     /* Size of the buffer */
+int AmountProduced = 3; /* Amount of items produced by a producer */
+int AmountConsumed = 3; /* Amount of items consumed by a consumer */
+int ProducerCount  = 2; /* Amount of producer threads*/
+int ConsumerCount  = 2; /* Amount of consumer threads*/
+int BufferSize     = 4; /* Size of the buffer */
 
 sem_t empty;
 sem_t full;
 int in  = 0;
 int out = 0;
-int buffer[BufferSize];
+int* buffer;
 pthread_mutex_t mutex;
 int do_output = 1;
 
@@ -56,15 +57,39 @@ static void* consumer(void* id)
 
 int main(int argc, char** argv)
 {
-  if (argc == 2 && strcmp(argv[1], "-q") == 0)
-    do_output = 0;
-  pthread_t pro[2];
-  pthread_t con[2];
+  char opt;
+  while ((opt = getopt(argc, argv, "c:C:p:P:q")) != -1) {
+    switch (opt) {
+      case 'q':
+        do_output = 0;
+        break;
+      case 'c':
+        AmountConsumed = atoi(optarg);
+        break;
+      case 'C':
+        ConsumerCount = atoi(optarg);
+        break;
+      case 'p':
+        AmountProduced = atoi(optarg);
+        break;
+      case 'P':
+        ProducerCount = atoi(optarg);
+        break;
+      case '?':
+        printf("unknown option: %c\n", optopt);
+        break;
+    }
+  }
+  pthread_t* pro = malloc(ProducerCount * sizeof(pthread_t));
+  pthread_t* con = malloc(ConsumerCount * sizeof(pthread_t));
+  buffer         = malloc(sizeof(int) * BufferSize);
   pthread_mutex_init(&mutex, NULL);
   sem_init(&empty, 0, BufferSize);
   sem_init(&full, 0, 0);
 
-  int ids[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; // The identity of each thread (for debug messages)
+  int* ids = malloc(sizeof(int) * ((ProducerCount + ConsumerCount)));
+  for (int i = 0; i < ProducerCount + ConsumerCount; i++)
+    ids[i] = i + 1; // The identity of each thread (for debug messages)
 
   for (int i = 0; i < ProducerCount; i++)
     pthread_create(&pro[i], NULL, producer, &ids[i]);
@@ -79,6 +104,9 @@ int main(int argc, char** argv)
   pthread_mutex_destroy(&mutex);
   sem_destroy(&empty);
   sem_destroy(&full);
+  free(pro);
+  free(con);
+  free(buffer);
 
   return 0;
 }