From 58ecc90355e2b311682a8136aec79e3dee279c14 Mon Sep 17 00:00:00 2001 From: Maged Michael Date: Mon, 8 Aug 2016 10:07:59 -0700 Subject: [PATCH] Methodology for using DeterministicSchedule support for auxiliary data and global invariants Summary: Depends on D3648195 This test example is intended to demonstrate the methodology for using DeterministicSchedule support for auxiliary data and global invariants. The main goal is fine-grained invariant checking, ideally after every shared update. The secondary goals are: - Minimize intrusion in the original code. In this proposed methodology, it is adding a friend. - Minimize duplication of original tested code. Unfortunately, depending on the original code, it seems that significant duplication may be unavoidable if we don't want to change the original code. This diff is primarily about the methodology for testing already developed code. I plan to apply what we agree on through this diff to the dynamic MPMCQueue code (D3462592). A future goal to keep in mind is creating a methodology for developing new code with hooks for DSched aux. data and invariant checking integrated in it, in order to minimize or eliminate duplication of tested code. In past projects, I used non-standard source code (basically algorithm code) that is automatically translatable through scripts and macros to input to a DSched-like tool as well as to compilable code. The main challenge for such a methodology is to allow the original source code to be standard readable C++ code. Reviewed By: djwatson Differential Revision: D3675447 fbshipit-source-id: aae2c9f0550af88dc3a5dcbe53318a75a86b6e2b --- folly/test/DeterministicScheduleTest.cpp | 152 +++++++++++++++++------ 1 file changed, 112 insertions(+), 40 deletions(-) diff --git a/folly/test/DeterministicScheduleTest.cpp b/folly/test/DeterministicScheduleTest.cpp index 36654856..6842b4a4 100644 --- a/folly/test/DeterministicScheduleTest.cpp +++ b/folly/test/DeterministicScheduleTest.cpp @@ -107,34 +107,115 @@ TEST(DeterministicSchedule, buggyAdd) { } // for bug } // TEST -/// Testing support for auxiliary variables and global invariants +/// Test support for auxiliary data and global invariants +/// -/** auxiliary variables for atomic counter test */ -struct AtomicCounterAux { - std::vector local_; +/// How to use DSched support for auxiliary data and global invariants: +/// 1. Forward declare an annotated shared class +/// 2. Add the annotated shared class as a friend of the original class(es) +/// to be tested +/// 3. Define auxiliary data +/// 4. Define function(s) for updating auxiliary data to match shared updates +/// 5. Define the annotated shared class +/// It supports an interface to the original class along with auxiliary +/// functions for updating aux data, checking invariants, and/or logging +/// It may have to duplicate the steps of multi-step operations in the +//// original code in order to manage aux data and check invariants after +/// shared accesses other than the first access in an opeeration +/// 6. Define function for checking global invariants and/or logging global +/// state +/// 7. Define function generator(s) for function object(s) that update aux +/// data, check invariants, and/or log state +/// 8. Define TEST using anotated shared data, aux data, and aux functions + +using DSched = DeterministicSchedule; +using AuxFn = std::function; + +/** forward declaration of annotated shared class */ +class AnnotatedAtomicCounter; + +/** original shared class to be tested */ +template class Atom = std::atomic> +class AtomicCounter { + friend AnnotatedAtomicCounter; - explicit AtomicCounterAux(int nthr) { + public: + explicit AtomicCounter(T val) : counter_(val) {} + + void inc() { + counter_.fetch_add(1); + } + + void inc_bug() { + int newval = counter_.load() + 1; + counter_.store(newval); + } + + T load() { + return counter_.load(); + } + + private: + Atom counter_ = {0}; +}; + +/** auxiliary data */ +struct AuxData { + explicit AuxData(int nthr) { local_.resize(nthr, 0); } + + std::vector local_; }; -/** auxiliary function for checking global invariants and logging - * steps of atomic counter test */ -void checkAtomicCounter( - int tid, - uint64_t step, - DeterministicAtomic& shared, - AtomicCounterAux& aux) { +/** aux update function(s) */ +void auxUpdateAfterInc(int tid, AuxData& auxdata, bool success) { + if (success) { + auxdata.local_[tid]++; + } +} + +/** annotated shared class */ +class AnnotatedAtomicCounter { + public: + explicit AnnotatedAtomicCounter(int val) : shared_(val) {} + + void inc(AuxFn& auxfn) { + DSched::setAux(auxfn); + /* calls the fine-grained original */ + shared_.inc(); + } + + void inc_bug(AuxFn auxfn) { + /* duplicates the steps of the multi-access original in order to + * annotate the second access */ + int newval = shared_.counter_.load() + 1; + DSched::setAux(auxfn); + shared_.counter_.store(newval); + } + + int load_direct() { + return shared_.counter_.load_direct(); + } + + private: + AtomicCounter shared_; +}; + +using Annotated = AnnotatedAtomicCounter; + +/** aux log & check function */ +void auxCheck(int tid, uint64_t step, Annotated& annotated, AuxData& auxdata) { /* read shared data */ - int val = shared.load_direct(); - /* read auxiliary variables */ + int val = annotated.load_direct(); + /* read auxiliary data */ int sum = 0; - for (int v : aux.local_) { + for (int v : auxdata.local_) { sum += v; } /* log state */ - VLOG(2) << "Step " << step << " -- tid " << tid << " -- shared counter " - << val << " -- sum increments " << sum; + VLOG(2) << "Step " << step << " -- tid " << tid + << " -- shared counter= " << val << " -- sum increments= " << sum; /* check invariant */ if (val != sum) { LOG(ERROR) << "Failed after step " << step; @@ -143,17 +224,11 @@ void checkAtomicCounter( } } -std::function auxAtomicCounter( - DeterministicAtomic& shared, - AtomicCounterAux& aux, - int tid) { - return [&shared, &aux, tid](uint64_t step, bool success) { - // update auxiliary data - if (success) { - aux.local_[tid]++; - } - // check invariants - checkAtomicCounter(tid, step, shared, aux); +/** function generator(s) */ +AuxFn auxAfterInc(int tid, Annotated& annotated, AuxData& auxdata) { + return [&annotated, &auxdata, tid](uint64_t step, bool success) { + auxUpdateAfterInc(tid, auxdata, success); + auxCheck(tid, step, annotated, auxdata); }; } @@ -170,30 +245,27 @@ TEST(DSchedCustom, atomic_add) { CHECK_GT(nthr, 0); - DeterministicAtomic counter{0}; - AtomicCounterAux auxData(nthr); - DeterministicSchedule sched(DeterministicSchedule::uniform(seed)); + Annotated annotated(0); + AuxData auxdata(nthr); + DSched sched(DSched::uniform(seed)); std::vector threads(nthr); for (int tid = 0; tid < nthr; ++tid) { - threads[tid] = DeterministicSchedule::thread([&, tid]() { - auto auxFn = auxAtomicCounter(counter, auxData, tid); + threads[tid] = DSched::thread([&, tid]() { + AuxFn auxfn = auxAfterInc(tid, annotated, auxdata); for (int i = 0; i < niter; ++i) { if (bug && (tid == 0) && (i % 10 == 0)) { - int newval = counter.load() + 1; - DeterministicSchedule::setAux(auxFn); - counter.store(newval); + annotated.inc_bug(auxfn); } else { - DeterministicSchedule::setAux(auxFn); - counter.fetch_add(1); + annotated.inc(auxfn); } } }); } for (auto& t : threads) { - DeterministicSchedule::join(t); + DSched::join(t); } - EXPECT_EQ(counter.load_direct(), nthr * niter); + EXPECT_EQ(annotated.load_direct(), nthr * niter); } int main(int argc, char** argv) { -- 2.34.1