-
-static void param_defaults(struct model_params *params)
-{
- params->maxreads = 0;
- params->fairwindow = 0;
- params->yieldon = false;
- params->yieldblock = false;
- params->enabledcount = 1;
- params->bound = 0;
- params->verbose = !!DBG_ENABLED();
- params->uninitvalue = 0;
- params->maxexecutions = 0;
-}
-
-static void model_main()
-{
- struct model_params params;
-
- param_defaults(¶ms);
-
- //parse_options(¶ms, main_argc, main_argv);
-
- //Initialize race detector
- initRaceDetector();
-
- snapshot_stack_init();
-
- model = new ModelChecker(params); // L: Model thread is created
-// install_trace_analyses(model->get_execution()); L: disable plugin
-
- snapshot_record(0);
- model->run();
- delete model;
-
- DEBUG("Exiting\n");
+extern "C" {
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp);
+}
+
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp) {
+ if (model) {
+ uint64_t time = rqtp->tv_sec * 1000000000 + rqtp->tv_nsec;
+ struct timespec currtime;
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+ uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+ model->switch_to_master(new ModelAction(THREAD_SLEEP, std::memory_order_seq_cst, time, lcurrtime));
+ if (rmtp != NULL) {
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+ uint64_t lendtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+ uint64_t elapsed = lendtime - lcurrtime;
+ rmtp->tv_sec = elapsed / 1000000000;
+ rmtp->tv_nsec = elapsed - rmtp->tv_sec * 1000000000;
+ }
+ }
+ return 0;