projects
/
model-checker-benchmarks.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
45862c2
)
ms-queue: strip down test driver
author
Brian Norris
<banorris@uci.edu>
Fri, 8 Mar 2013 01:56:23 +0000
(17:56 -0800)
committer
Brian Norris
<banorris@uci.edu>
Fri, 8 Mar 2013 02:03:09 +0000
(18:03 -0800)
+ a few assertions
ms-queue/main.c
patch
|
blob
|
history
diff --git
a/ms-queue/main.c
b/ms-queue/main.c
index 210c57a1e208518c6dca9558d0c9d9357e88ca19..c09470de2b22f3760d4b3e2fcb2ee3c3b3e0b195 100644
(file)
--- a/
ms-queue/main.c
+++ b/
ms-queue/main.c
@@
-1,14
+1,15
@@
#include <stdlib.h>
#include <stdlib.h>
-#include <assert.h>
#include <stdio.h>
#include <threads.h>
#include "my_queue.h"
#include <stdio.h>
#include <threads.h>
#include "my_queue.h"
+#include "model-assert.h"
static int procs = 2;
static int procs = 2;
-static int iterations = 1;
static queue_t *queue;
static thrd_t *threads;
static queue_t *queue;
static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
static int num_threads;
int get_thread_num()
static int num_threads;
int get_thread_num()
@@
-18,42
+19,23
@@
int get_thread_num()
for (i = 0; i < num_threads; i++)
if (curr.priv == threads[i].priv)
return i;
for (i = 0; i < num_threads; i++)
if (curr.priv == threads[i].priv)
return i;
-
assert
(0);
+
MODEL_ASSERT
(0);
return -1;
}
return -1;
}
-static void parse_args(int argc, char **argv)
-{
- extern char *optarg;
- int c;
-
- while ((c = getopt(argc, argv, "i:p:")) != EOF) {
- switch (c) {
- case 'i':
- iterations = atoi(optarg);
- break;
- case 'p':
- procs = atoi(optarg);
- break;
- default:
- assert(0);
- }
- }
-}
-
static void main_task(void *param)
{
static void main_task(void *param)
{
- unsigned int i, j;
unsigned int val;
int pid = *((int *)param);
unsigned int val;
int pid = *((int *)param);
- for (i = 0; i < iterations; i++) {
- val = 1 + pid * iterations + i;
- printf("worker %d, enqueueing: %u\n", pid, val);
- enqueue(queue, val);
-
- val = dequeue(queue);
- printf("worker %d, dequeued: %u\n", pid, val);
+ if (!pid) {
+ input[0] = 17;
+ enqueue(queue, input[0]);
+ output[0] = dequeue(queue);
+ } else {
+ input[1] = 37;
+ enqueue(queue, input[1]);
+ output[1] = dequeue(queue);
}
}
}
}
@@
-61,15
+43,17
@@
int user_main(int argc, char **argv)
{
int i;
int *param;
{
int i;
int *param;
-
-
parse_args(argc, argv)
;
+ unsigned int in_sum = 0, out_sum = 0;
+
int zero = 0
;
queue = calloc(1, sizeof(*queue));
queue = calloc(1, sizeof(*queue));
-
assert
(queue);
+
MODEL_ASSERT
(queue);
num_threads = procs;
threads = malloc(num_threads * sizeof(thrd_t));
param = malloc(num_threads * sizeof(*param));
num_threads = procs;
threads = malloc(num_threads * sizeof(thrd_t));
param = malloc(num_threads * sizeof(*param));
+ input = calloc(num_threads, sizeof(*input));
+ output = calloc(num_threads, sizeof(*output));
init_queue(queue, num_threads);
for (i = 0; i < num_threads; i++) {
init_queue(queue, num_threads);
for (i = 0; i < num_threads; i++) {
@@
-79,6
+63,19
@@
int user_main(int argc, char **argv)
for (i = 0; i < num_threads; i++)
thrd_join(threads[i]);
for (i = 0; i < num_threads; i++)
thrd_join(threads[i]);
+ for (i = 0; i < num_threads; i++) {
+ in_sum += input[i];
+ out_sum += output[i];
+ }
+ for (i = 0; i < num_threads; i++)
+ printf("input[%d] = %u\n", i, input[i]);
+ for (i = 0; i < num_threads; i++) {
+ if (output[i] == 0)
+ zero = 1; /* A zero result means queue was empty */
+ printf("output[%d] = %u\n", i, output[i]);
+ }
+ MODEL_ASSERT(in_sum == out_sum || zero);
+
free(param);
free(threads);
free(queue);
free(param);
free(threads);
free(queue);