From d4e437ba8e99a9cd38c4ccb1c243427935c8f293 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Thu, 26 Feb 2009 18:13:46 -0500 Subject: [PATCH] Fix makefile, set default nesting to 2 Signed-off-by: Mathieu Desnoyers --- formal-model/urcu/Makefile | 18 +++++++++--------- formal-model/urcu/urcu.spin | 7 ++++--- 2 files changed, 13 insertions(+), 12 deletions(-) diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile index 498241b..4488219 100644 --- a/formal-model/urcu/Makefile +++ b/formal-model/urcu/Makefile @@ -93,8 +93,8 @@ urcu_free_single_flip_define: urcu_free_ltl: touch .input.define - cat DEFINES > pan.ltl cat .input.define >> pan.ltl + cat DEFINES >> pan.ltl spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl # Progress checks @@ -109,8 +109,8 @@ urcu_progress_writer_define: urcu_progress_writer_ltl: touch .input.define - cat DEFINES > pan.ltl - cat .input.define >> pan.ltl + cat .input.define > pan.ltl + cat DEFINES >> pan.ltl spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl urcu_progress_reader: clean urcu_progress_reader_ltl \ @@ -123,8 +123,8 @@ urcu_progress_reader_define: urcu_progress_reader_ltl: touch .input.define - cat DEFINES > pan.ltl - cat .input.define >> pan.ltl + cat .input.define > pan.ltl + cat DEFINES >> pan.ltl spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl urcu_progress_writer_error: clean urcu_progress_writer_error_ltl \ @@ -137,8 +137,8 @@ urcu_progress_writer_error_define: urcu_progress_writer_error_ltl: touch .input.define - cat .input.define >> pan.ltl - cat DEFINES > pan.ltl + cat .input.define > pan.ltl + cat DEFINES >> pan.ltl spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl @@ -152,8 +152,8 @@ pan: pan.c gcc -w ${CFLAGS} -o pan pan.c pan.c: pan.ltl ${SPINFILE} - cat .input.define >> .input.spin - cat DEFINES > .input.spin + cat .input.define > .input.spin + cat DEFINES >> .input.spin cat ${SPINFILE} >> .input.spin rm -f .input.spin.trail spin -a -X -N pan.ltl .input.spin diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin index 17c6612..903782b 100644 --- a/formal-model/urcu/urcu.spin +++ b/formal-model/urcu/urcu.spin @@ -209,7 +209,8 @@ progress_reader: ooo_mem(i); WRITE_CACHED_VAR(urcu_active_readers_one, tmp2); :: else -> - WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1); + WRITE_CACHED_VAR(urcu_active_readers_one, + tmp + 1); fi; ooo_mem(i); smp_mb(i); @@ -285,7 +286,7 @@ progress_writer1: //smp_mc(i); wait_for_quiescent_state(tmp, i, j); //smp_mc(i); - #ifndef SINGLE_FLIP +#ifndef SINGLE_FLIP ooo_mem(i); tmp = READ_CACHED_VAR(urcu_gp_ctr); ooo_mem(i); @@ -293,7 +294,7 @@ progress_writer1: //smp_mc(i); ooo_mem(i); wait_for_quiescent_state(tmp, i, j); - #endif +#endif ooo_mem(i); smp_mb(i); ooo_mem(i); -- 2.34.1