The previous instance size resulted in a timeout now that the DPOR
reduction is less efficient (because it's less buggy)
# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
! ignore .*LD_PRELOAD.*
# 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] [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)
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.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;
sem_t empty;
sem_t full;
int in = 0;
int out = 0;
pthread_mutex_t mutex;
int do_output = 1;
pthread_mutex_t mutex;
int do_output = 1;
int main(int argc, char** argv)
{
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);
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]);
for (int i = 0; i < ProducerCount; i++)
pthread_create(&pro[i], NULL, producer, &ids[i]);
pthread_mutex_destroy(&mutex);
sem_destroy(&empty);
sem_destroy(&full);
pthread_mutex_destroy(&mutex);
sem_destroy(&empty);
sem_destroy(&full);
+ free(pro);
+ free(con);
+ free(buffer);