printf -> model_print

As we move toward redirecting program output, we will need a special
printf function for model-checking prints. Just define a simple
model_print() for now.

diff --git a/action.cc b/action.cc
index 1387ed15b67c9ac25d7fcba68491bbb72d8ff236..486e89ee54aaddc8ea302c64b3a1eccef786a28c 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -468,22 +468,22 @@ void ModelAction::print() const
                break;
        }
 
                break;
        }
 

-       printf("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,
+       model_print("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,

                        seq_number, id_to_int(tid), type_str, mo_str, location, valuetoprint);
        if (is_read()) {
                if (reads_from)
                        seq_number, id_to_int(tid), type_str, mo_str, location, valuetoprint);
        if (is_read()) {
                if (reads_from)

-                       printf("  Rf: %-3d", reads_from->get_seq_number());
+                       model_print("  Rf: %-3d", reads_from->get_seq_number());

                else
                else

-                       printf("  Rf: ?  ");
+                       model_print("  Rf: ?  ");

        }
        if (cv) {
                if (is_read())
        }
        if (cv) {
                if (is_read())

-                       printf(" ");
+                       model_print(" ");

                else
                else

-                       printf("          ");
+                       model_print("          ");

                cv->print();
        } else
                cv->print();
        } else

-               printf("\n");
+               model_print("\n");

 }
 
 /** @brief Print nicely-formatted info about this ModelAction */
 }
 
 /** @brief Print nicely-formatted info about this ModelAction */

diff --git a/clockvector.cc b/clockvector.cc
index e56c2ace662507be12875c18446932fe54593252..6cd943b835b2ec2915b992101549961f622ec4ee 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -89,7 +89,7 @@ modelclock_t ClockVector::getClock(thread_id_t thread) {
 void ClockVector::print() const
 {
        int i;
 void ClockVector::print() const
 {
        int i;

-       printf("CV: (");
+       model_print("CV: (");

        for (i = 0; i < num_threads; i++)
        for (i = 0; i < num_threads; i++)

-               printf("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+               model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");

 }
 }

diff --git a/common.cc b/common.cc
index f37f92f1ba7434cdddd365564048b711ddc40816..d9915993c8535c0b9b99ee3ffe0f27ab9aa9ec80 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -24,10 +24,10 @@ void print_trace(void)
        size = backtrace(array, MAX_TRACE_LEN);
        strings = backtrace_symbols(array, size);
 
        size = backtrace(array, MAX_TRACE_LEN);
        strings = backtrace_symbols(array, size);
 

-       printf("\nDumping stack trace (%d frames):\n", size);
+       model_print("\nDumping stack trace (%d frames):\n", size);

 
        for (i = 0; i < size; i++)
 
        for (i = 0; i < size; i++)

-               printf("\t%s\n", strings[i]);
+               model_print("\t%s\n", strings[i]);

 
        free(strings);
 #endif /* CONFIG_STACKTRACE */
 
        free(strings);
 #endif /* CONFIG_STACKTRACE */


@@ -40,7 +40,7 @@ void model_print_summary(void)
 
 void assert_hook(void)
 {
 
 void assert_hook(void)
 {

-       printf("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__);
+       model_print("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__);

 }
 
 void model_assert(bool expr, const char *file, int line)
 }
 
 void model_assert(bool expr, const char *file, int line)

diff --git a/common.h b/common.h
index 81b26728d917c0af8c1b26e9d0fa2d28cccb8a5a..b1d6b31ecfe89e4136cee5a368e27534283c0bd6 100644 (file)
--- a/common.h
+++ b/common.h
@@ -8,8 +8,10 @@
 #include <stdio.h>
 #include "config.h"
 
 #include <stdio.h>
 #include "config.h"
 

+#define model_print(fmt, ...) do { printf(fmt, ##__VA_ARGS__); } while (0)
+

 #ifdef CONFIG_DEBUG
 #ifdef CONFIG_DEBUG

-#define DEBUG(fmt, ...) do { printf("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
+#define DEBUG(fmt, ...) do { model_print("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)

 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else
 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else

diff --git a/hashtable.h b/hashtable.h
index 4d3b7de8e9a7b9e8d270b543c8dbc8315a664965..d5c69ccba8456ad4930dcbdee93f3f5d229caca3 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -9,6 +9,7 @@
 #include <stdio.h>
 #include <string.h>
 #include "mymemory.h"
 #include <stdio.h>
 #include <string.h>
 #include "mymemory.h"

+#include "common.h"

 
 /**
  * Hashtable linked node class, for chained storage of hash table conflicts. By
 
 /**
  * Hashtable linked node class, for chained storage of hash table conflicts. By


@@ -161,7 +162,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
                unsigned int oldcapacity = capacity;
 
                if((newtable = (struct hashlistnode<_Key,_Val> *) _calloc(newsize, sizeof(struct hashlistnode<_Key,_Val>))) == NULL) {
                unsigned int oldcapacity = capacity;
 
                if((newtable = (struct hashlistnode<_Key,_Val> *) _calloc(newsize, sizeof(struct hashlistnode<_Key,_Val>))) == NULL) {

-                       printf("Calloc error %s %d\n", __FILE__, __LINE__);
+                       model_print("Calloc error %s %d\n", __FILE__, __LINE__);

                        exit(-1);
                }
                
                        exit(-1);
                }
                

diff --git a/main.cc b/main.cc
index fb4acbe75d6b530feabc4e76b111cc0f4bf4b29d..10e2d3b93eae2e3c80e4569464e44a9ebb63d17a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -28,7 +28,7 @@ static void print_usage(struct model_params *params) {
        /* Reset defaults before printing */
        param_defaults(params);
 
        /* Reset defaults before printing */
        param_defaults(params);
 

-       printf(
+       model_print(

 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
 "\n"
 "Options:\n"
 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
 "\n"
 "Options:\n"

diff --git a/model.cc b/model.cc
index 05e767981554a0c301169905a95ea5081d3cb8c0..8dcb6f3ad8e69a0e82ad3991c4425a35f1a24640 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -27,7 +27,7 @@ struct bug_message {
        ~bug_message() { if (msg) snapshot_free(msg); }
 
        char *msg;
        ~bug_message() { if (msg) snapshot_free(msg); }
 
        char *msg;

-       void print() { printf("%s", msg); }
+       void print() { model_print("%s", msg); }

 
        SNAPSHOTALLOC
 };
 
        SNAPSHOTALLOC
 };


@@ -373,7 +373,7 @@ bool ModelChecker::have_bug_reports() const
 void ModelChecker::print_bugs() const
 {
        if (have_bug_reports()) {
 void ModelChecker::print_bugs() const
 {
        if (have_bug_reports()) {

-               printf("Bug report: %zu bug%s detected\n",
+               model_print("Bug report: %zu bug%s detected\n",

                                priv->bugs.size(),
                                priv->bugs.size() > 1 ? "s" : "");
                for (unsigned int i = 0; i < priv->bugs.size(); i++)
                                priv->bugs.size(),
                                priv->bugs.size() > 1 ? "s" : "");
                for (unsigned int i = 0; i < priv->bugs.size(); i++)


@@ -401,11 +401,11 @@ void ModelChecker::record_stats()
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {

-       printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
-       printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
-       printf("Number of infeasible executions: %d\n", stats.num_infeasible);
-       printf("Total executions: %d\n", stats.num_total);
-       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+       model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
+       model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
+       model_print("Total executions: %d\n", stats.num_total);
+       model_print("Total nodes created: %d\n", node_stack->get_total_nodes());

 }
 
 /**
 }
 
 /**


@@ -422,11 +422,11 @@ bool ModelChecker::next_execution()
        record_stats();
 
        if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
        record_stats();
 
        if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {

-               printf("Earliest divergence point since last feasible execution:\n");
+               model_print("Earliest divergence point since last feasible execution:\n");

                if (earliest_diverge)
                        earliest_diverge->print();
                else
                if (earliest_diverge)
                        earliest_diverge->print();
                else

-                       printf("(Not set)\n");
+                       model_print("(Not set)\n");

 
                earliest_diverge = NULL;
 
 
                earliest_diverge = NULL;
 


@@ -435,11 +435,11 @@ bool ModelChecker::next_execution()
 
                checkDataRaces();
                print_bugs();
 
                checkDataRaces();
                print_bugs();

-               printf("\n");
+               model_print("\n");

                print_stats();
                print_summary();
        } else if (DBG_ENABLED()) {
                print_stats();
                print_summary();
        } else if (DBG_ENABLED()) {

-               printf("\n");
+               model_print("\n");

                print_summary();
        }
 
                print_summary();
        }
 


@@ -447,7 +447,7 @@ bool ModelChecker::next_execution()
                return false;
 
        if (DBG_ENABLED()) {
                return false;
 
        if (DBG_ENABLED()) {

-               printf("Next execution will diverge at:\n");
+               model_print("Next execution will diverge at:\n");

                diverge->print();
        }
 
                diverge->print();
        }
 


@@ -2198,11 +2198,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                assert_bug("May read from uninitialized atomic");
 
        if (DBG_ENABLED() || !initialized) {
                assert_bug("May read from uninitialized atomic");
 
        if (DBG_ENABLED() || !initialized) {

-               printf("Reached read action:\n");
+               model_print("Reached read action:\n");

                curr->print();
                curr->print();

-               printf("Printing may_read_from\n");
+               model_print("Printing may_read_from\n");

                curr->get_node()->print_may_read_from();
                curr->get_node()->print_may_read_from();

-               printf("End printing may_read_from\n");
+               model_print("End printing may_read_from\n");

        }
 }
 
        }
 }
 


@@ -2226,16 +2226,16 @@ static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;
 
 {
        action_list_t::iterator it;
 

-       printf("---------------------------------------------------------------------\n");
-       printf("Trace:\n");
+       model_print("---------------------------------------------------------------------\n");
+       model_print("Trace:\n");

        unsigned int hash=0;
 
        for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
                hash=hash^(hash<<3)^((*it)->hash());
        }
        unsigned int hash=0;
 
        for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
                hash=hash^(hash<<3)^((*it)->hash());
        }

-       printf("HASH %u\n", hash);
-       printf("---------------------------------------------------------------------\n");
+       model_print("HASH %u\n", hash);
+       model_print("---------------------------------------------------------------------\n");

 }
 
 #if SUPPORT_MOD_ORDER_DUMP
 }
 
 #if SUPPORT_MOD_ORDER_DUMP


@@ -2278,9 +2278,9 @@ void ModelChecker::print_summary()
 #endif
 
        if (!isfinalfeasible())
 #endif
 
        if (!isfinalfeasible())

-               printf("INFEASIBLE EXECUTION!\n");
+               model_print("INFEASIBLE EXECUTION!\n");

        print_list(action_trace);
        print_list(action_trace);

-       printf("\n");
+       model_print("\n");

 }
 
 /**
 }
 
 /**


@@ -2415,7 +2415,7 @@ bool ModelChecker::take_step() {
         */
        if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
                        isfinalfeasible() && !unrealizedraces.empty()) {
         */
        if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
                        isfinalfeasible() && !unrealizedraces.empty()) {

-               printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+               model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",

                                pending_rel_seqs->size());
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,
                                pending_rel_seqs->size());
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,

diff --git a/mymemory.cc b/mymemory.cc
index 5922a32d19f63491d556a275cb2d25be5bf510da..6ea6b92927c4ddebabe5b690b13800667a70fd08 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -135,7 +135,7 @@ void * HandleEarlyAllocationRequest(size_t sz)
        sz = (sz + 7) & ~7;
 
        if (sz > (BOOTSTRAPBYTES-offset)) {
        sz = (sz + 7) & ~7;
 
        if (sz > (BOOTSTRAPBYTES-offset)) {

-               printf("OUT OF BOOTSTRAP MEMORY\n");
+               model_print("OUT OF BOOTSTRAP MEMORY\n");

                exit(EXIT_FAILURE);
        }
 
                exit(EXIT_FAILURE);
        }
 

diff --git a/nodestack.cc b/nodestack.cc
index b4f75e0336a3afdc3978b7ecb086e459423df455..4da3cd60fd7db93c147fba60faf929d6fccb9a0f 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -91,7 +91,7 @@ void Node::print()
        if (action)
                action->print();
        else
        if (action)
                action->print();
        else

-               printf("******** empty action ********\n");
+               model_print("******** empty action ********\n");

 }
 
 /** @brief Prints info about may_read_from set */
 }
 
 /** @brief Prints info about may_read_from set */


@@ -495,14 +495,14 @@ NodeStack::~NodeStack()
 
 void NodeStack::print()
 {
 
 void NodeStack::print()
 {

-       printf("............................................\n");
-       printf("NodeStack printing node_list:\n");
+       model_print("............................................\n");
+       model_print("NodeStack printing node_list:\n");

        for (unsigned int it = 0; it < node_list.size(); it++) {
                if (it == this->iter)
        for (unsigned int it = 0; it < node_list.size(); it++) {
                if (it == this->iter)

-                       printf("vvv following action is the current iterator vvv\n");
+                       model_print("vvv following action is the current iterator vvv\n");

                node_list[it]->print();
        }
                node_list[it]->print();
        }

-       printf("............................................\n");
+       model_print("............................................\n");

 }
 
 /** Note: The is_enabled set contains what actions were enabled when
 }
 
 /** Note: The is_enabled set contains what actions were enabled when

diff --git a/snapshot.cc b/snapshot.cc
index fb00d1511c8505df3c34fc22eaa0b7adad838937..e930a33622ce9dbb89463cd77b0447f84de7f45c 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -19,10 +19,10 @@
 
 #include "common.h"
 
 
 #include "common.h"
 

-#define FAILURE(mesg) { printf("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit(EXIT_FAILURE); }
+#define FAILURE(mesg) { model_print("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit(EXIT_FAILURE); }

 
 #ifdef CONFIG_SSDEBUG
 
 #ifdef CONFIG_SSDEBUG

-#define SSDEBUG                printf
+#define SSDEBUG                model_print

 #else
 #define SSDEBUG(...)   do { } while (0)
 #endif
 #else
 #define SSDEBUG(...)   do { } while (0)
 #endif


@@ -86,9 +86,9 @@ static void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsna
  */
 static void HandlePF( int sig, siginfo_t *si, void * unused){
        if( si->si_code == SEGV_MAPERR ){
  */
 static void HandlePF( int sig, siginfo_t *si, void * unused){
        if( si->si_code == SEGV_MAPERR ){

-               printf("Real Fault at %p\n", si->si_addr);
+               model_print("Real Fault at %p\n", si->si_addr);

                print_trace();
                print_trace();

-               printf("For debugging, place breakpoint at: %s:%d\n",
+               model_print("For debugging, place breakpoint at: %s:%d\n",

                                __FILE__, __LINE__);
                exit( EXIT_FAILURE );
        }
                                __FILE__, __LINE__);
                exit( EXIT_FAILURE );
        }


@@ -96,7 +96,7 @@ static void HandlePF( int sig, siginfo_t *si, void * unused){
 
        unsigned int backingpage=snapshotrecord->lastBackingPage++; //Could run out of pages...
        if (backingpage==snapshotrecord->maxBackingPages) {
 
        unsigned int backingpage=snapshotrecord->lastBackingPage++; //Could run out of pages...
        if (backingpage==snapshotrecord->maxBackingPages) {

-               printf("Out of backing pages at %p\n", si->si_addr);
+               model_print("Out of backing pages at %p\n", si->si_addr);

                exit( EXIT_FAILURE );
        }
 
                exit( EXIT_FAILURE );
        }
 


@@ -151,12 +151,12 @@ void initSnapshotLibrary(unsigned int numbackingpages,
        sa.sa_sigaction = HandlePF;
 #ifdef MAC
        if( sigaction( SIGBUS, &sa, NULL ) == -1 ){
        sa.sa_sigaction = HandlePF;
 #ifdef MAC
        if( sigaction( SIGBUS, &sa, NULL ) == -1 ){

-               printf("SIGACTION CANNOT BE INSTALLED\n");
+               model_print("SIGACTION CANNOT BE INSTALLED\n");

                exit(EXIT_FAILURE);
        }
 #endif
        if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){
                exit(EXIT_FAILURE);
        }
 #endif
        if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){

-               printf("SIGACTION CANNOT BE INSTALLED\n");
+               model_print("SIGACTION CANNOT BE INSTALLED\n");

                exit(EXIT_FAILURE);
        }
 
                exit(EXIT_FAILURE);
        }
 


@@ -251,7 +251,7 @@ void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
 #if USE_MPROTECT_SNAPSHOT
        unsigned int memoryregion=snapshotrecord->lastRegion++;
        if (memoryregion==snapshotrecord->maxRegions) {
 #if USE_MPROTECT_SNAPSHOT
        unsigned int memoryregion=snapshotrecord->lastRegion++;
        if (memoryregion==snapshotrecord->maxRegions) {

-               printf("Exceeded supported number of memory regions!\n");
+               model_print("Exceeded supported number of memory regions!\n");

                exit(EXIT_FAILURE);
        }
 
                exit(EXIT_FAILURE);
        }
 


@@ -268,13 +268,13 @@ snapshot_id takeSnapshot( ){
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ ) == -1 ){
                        perror("mprotect");
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ ) == -1 ){
                        perror("mprotect");

-                       printf("Failed to mprotect inside of takeSnapShot\n");
+                       model_print("Failed to mprotect inside of takeSnapShot\n");

                        exit(EXIT_FAILURE);
                }
        }
        unsigned int snapshot=snapshotrecord->lastSnapShot++;
        if (snapshot==snapshotrecord->maxSnapShots) {
                        exit(EXIT_FAILURE);
                }
        }
        unsigned int snapshot=snapshotrecord->lastSnapShot++;
        if (snapshot==snapshotrecord->maxSnapShots) {

-               printf("Out of snapshots\n");
+               model_print("Out of snapshots\n");

                exit(EXIT_FAILURE);
        }
        snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;
                exit(EXIT_FAILURE);
        }
        snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;


@@ -305,7 +305,7 @@ void rollBack( snapshot_id theID ){
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){
                        perror("mprotect");
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){
                        perror("mprotect");

-                       printf("Failed to mprotect inside of takeSnapShot\n");
+                       model_print("Failed to mprotect inside of takeSnapShot\n");

                        exit(EXIT_FAILURE);
                }
        }
                        exit(EXIT_FAILURE);
                }
        }

diff --git a/threads.cc b/threads.cc
index dc2db2d9bfefcab57458035f3f4bc815b75b5fc5..dd2a59832027557b543d8fd606f842527b270f97 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -161,7 +161,7 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
        /* Initialize state */
        ret = create_context();
        if (ret)
        /* Initialize state */
        ret = create_context();
        if (ret)

-               printf("Error in create_context\n");
+               model_print("Error in create_context\n");

 
        id = model->get_next_id();
        *user_thread = id;
 
        id = model->get_next_id();
        *user_thread = id;