ModelCheck.cpp

Go to the documentation of this file.

/** @file ModelCheck.cpp
* @author Gabor Madl
* @date Created 08/2005
* @brief Model Checker library.
* @warning This library is experimental.
*
*
* =================================================================
* DREAM License v2.0
* 
* DREAM - Distributed Real-time Embedded Analysis Method
* http://dre.sourceforge.net.
* Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.
* 
* This file is part of DREAM.
* 
* DREAM is free software; you can redistribute it and/or modify it
* under the terms of the GNU General Public License version 2 as
* published by the Free Software Foundation. No future versions of
* the GPL license may be automatically applied to DREAM. It is in
* the sole discretion of the copyright holder to determine whether
* DREAM may be released under a different license or terms. There
* are no restrictions on the use of DREAM for any purpose.
* 
* DREAM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
* 
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
* MA 02110-1301, USA.
* 
* By submitting comments, suggestions, code, code snippets,
* techniques (including that of usage), and algorithms, submitters
* acknowledge that they have the right to do so, that any such
* submissions are given freely and unreservedly, and that they
* waive any claims to copyright or ownership. In addition,
* submitters acknowledge that any such submission might become
* part of the copyright maintained on the overall body of code,
* which comprises DREAM. By making a submission, submitter agrees
* to these terms. Furthermore, submitters acknowledge that the
* incorporation or modification of such submissions is entirely
* at the discretion of the moderators of the DREAM project.
* 
* DREAM links to the Libxml2 third party library. Please see 
* COPYING-libxml for the copyright information of Libxml2.
* =================================================================
*/

#include "ModelCheck.h"

namespace DREAM
{

ModelCheck::ModelCheck (DREAM::System* system_ptr)
: system_ptr_ (system_ptr), endtoend_ (0.0)
{
}

bool ModelCheck::branching_point (DREAM::NODE_AVLTREE* node_avltree, bool verbose)
{
        DREAM::Context contextvalue;

#ifdef DREAM_RACE_CONDITION
        if (Option::race_condition_)
        {
                // Iterate through priority inversion list
                if (system_ptr_->inversion ())
                        return true;
                else
                        system_ptr_->destroy_priority_list ();
        }
#endif
        DREAM::NODE_AVLTREE::iterator node_iter;

        for (node_iter = node_avltree->begin (); node_iter != node_avltree->end (); node_iter++)
        {
                contextvalue = node_iter->second->context ();

#ifdef DREAM_BRANCHING
                if ((contextvalue == branchingpoint) && (Option::branching_))
                {
                        node_iter->second->branching_point ();
                        return true;
                }
                else 
#endif
                if (contextvalue == worstcase)
                {
                        node_iter->second->context (bestcase);
                        return true;
                }
                else
                {
                        node_iter->second->context (worstcase);
                }
        }

        return false;
}

bool ModelCheck::random_testing (DREAM::System* system_ptr, bool verbose)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        endtoend_ = 0.0;
        double temp;
        time_t start_time, start_block, end_block;
        time (&start_time);
        time (&start_block);

        if (verbose)
        {
                std::cout << std::endl << "Testing " << Option::number_of_repetitions_ << " random cases." << std::endl;
                if (19999 < Option::number_of_repetitions_)
                {
                        std::cout << "Reporting partial results after 10^4 simulations." << std::endl << std::endl;
                        std::cout << "============================================================================" << std::endl;
                        std::cout << " 10^4 sim time\t| Avg trace sim time\t| End-to-end performance" << std::endl;
                        std::cout << "----------------------------------------------------------------------------" << std::endl;
                }
        }

        DREAM::Solution solution (system_ptr);

        uint i, j = 0;
        for (i = 0; i < Option::number_of_repetitions_; i++)
        {
                if (solution.fitness (Option::verbose1_, false, &temp) != 0.0)
                {
                        if (endtoend_ < temp) endtoend_ = temp;

                        if (verbose)
                        {
                                // Repeat simulation to show execution trace that has missed the deadline
                                DREAM::NODE_MAP task_map;
                                DREAM::NODE_MAP channel_map;
                                DREAM::NODE_MAP timer_map;

                                system_ptr->visitor_map (&task_map, &channel_map, &timer_map);

                                for (DREAM::NODE_MAP::const_iterator node_map_iter = task_map.begin (); node_map_iter != task_map.end (); node_map_iter++)
                                        node_map_iter->second->context (repeat);

                                for (DREAM::NODE_MAP::const_iterator node_map_iter = channel_map.begin (); node_map_iter != channel_map.end (); node_map_iter++)
                                        node_map_iter->second->context (repeat);

                                for (DREAM::NODE_MAP::const_iterator node_map_iter = timer_map.begin (); node_map_iter != timer_map.end (); node_map_iter++)
                                        node_map_iter->second->context (repeat);

                                system_ptr->reset ();
                                system_ptr->simulate (true, false, &temp);

                                time_t end_time;
                                time (&end_time);
                                uint perf = end_time - start_time;
//                              std::cout << "System is unschedulable." << std::endl;
                                std::cout << "Analysis time: " << perf << " seconds." << std::endl;
                                std::cout << "Worst case end-to-end performance encountered: " << endtoend_ << std::endl;
                        }

                        return false;
                }
                if (endtoend_ < temp) endtoend_ = temp;

                if (++j == 10000)
                {
                        time_t end_block;
                        time (&end_block);
                        uint block = end_block - start_block;
                        std::cout << " " << block << " secs\t\t| " << std::fixed << std::setprecision (1) << (double)block/10 << " ms\t\t| " << endtoend_ << std::endl;
                        j = 0;
                        time (&start_block);
                }
        }

        if (verbose)
        {
                time_t end_time;
                time (&end_time);
                uint perf = end_time - start_time;
                std::cout << "Analysis complete. No errors found." << std::endl;
                std::cout << "Analysis time: " << perf << " seconds." << std::endl;
                std::cout << "Worst case end-to-end performance: " << endtoend_ << std::endl;
        }

        return true;
}
        
bool ModelCheck::trace_based_model_check (DREAM::System* system_ptr, bool verbose)
        throw (DREAM::Exception)
{
        endtoend_ = 0.0;
        double temp;
        time_t start_time, start_block, end_block;
        time (&start_time);
        time (&start_block);

        if (verbose)
                std::cout << std::endl << "Model checking DREAM model." << std::endl << std::endl;

        DREAM::Solution solution (system_ptr);

        if (!solution.deterministic ())
                throw DREAM::Exception ("Model checking is supported on deterministic sub-priorities only (same sub-priorities are disallowed). Try to optimize the scheduling first...");

        DREAM::SCHEDULER_MAP::const_iterator scheduler_iter;

        for (scheduler_iter = system_ptr->scheduler_map ()->begin (); scheduler_iter != system_ptr->scheduler_map ()->end (); scheduler_iter++)
        {
                if (scheduler_iter->second->threadpoolsize () > 1)
                        throw DREAM::Exception ("ModelCheck::trace_based_model_check () currently can ony be used to check non-preemptive systems with no thread pools.");
        }

        DREAM::NODE_AVLTREE mc_queue;
        DREAM::NODE_MAP::const_iterator node_map_iter;
        DREAM::NODE_AVLTREE::const_iterator node_iter;
        DREAM::NODE_MAP::const_iterator node_iter2;
        
        DREAM::NODE_MAP task_map;
        DREAM::NODE_MAP channel_map;
        DREAM::NODE_MAP timer_map;

        system_ptr->visitor_map (&task_map, &channel_map, &timer_map);

        for (node_map_iter = task_map.begin (); node_map_iter != task_map.end (); node_map_iter++)
        {
                // If Task with bcet found put it in a queue
                if (node_map_iter->second->bcet () != node_map_iter->second->wcet ())
                {
                        mc_queue.insert (node_map_iter->first, node_map_iter->second);
                }
        }

        for (node_map_iter = channel_map.begin (); node_map_iter != channel_map.end (); node_map_iter++)
        {
                // If Channel with bcet found put it in a queue
                if (node_map_iter->second->bcet () != node_map_iter->second->wcet ())
                {
                        mc_queue.insert (node_map_iter->first, node_map_iter->second);
                }
        }

        bool drifting = false;
        for (node_map_iter = timer_map.begin (); node_map_iter != timer_map.end (); node_map_iter++)
        {
                // If Timer with bcet found put it in a queue
                if (node_map_iter->second->bcet () != node_map_iter->second->wcet ())
                {
                        mc_queue.insert (node_map_iter->first, node_map_iter->second);
                        drifting = true;
                }
        }

        if (verbose)
        {
                if (drifting)
                        std::cout << std::endl << std::endl << "WARNING: Arbitrarily drifting clocks found. This model is too permissive and probably cannot be verified using finite simulation time." << std::endl << std::endl;
        }

        // Initialize wcet times
        for (node_iter = mc_queue.begin (); node_iter != mc_queue.end (); node_iter++)
        {
                node_iter->second->context (worstcase);
                node_iter->second->remote_dep (false);
        }

        // Check for remote dependents
        const DREAM::NODE_MAP* node_map;
        uint remote_deps = 0;

        for (node_iter = mc_queue.begin (); node_iter != mc_queue.end (); node_iter++)
        {
                node_map = node_iter->second->get_dependent_map ();

                for (node_iter2 = node_map->begin (); node_iter2 != node_map->end (); node_iter2++)
                {
                        // Check for immediate dependents
                        if (node_iter->second->scheduler () != node_iter2->second->scheduler ())
                        {
                                node_iter->second->remote_dep (true);
                        }
                }
        }

        // Count remote dependencies
        for (node_iter = mc_queue.begin (); node_iter != mc_queue.end (); node_iter++)
        {
                if (node_iter->second->remote_dep ())
                        remote_deps++;
        }

        if (verbose)
        {
                std::cout << "Number of nodes with remote dependencies: " << remote_deps << " out of " << mc_queue.size () << "." << std::endl;
                std::cout << std::endl << "Verification in progress..." << std::endl;

                std::cout << "Reporting partial results after 10^4 simulations." << std::endl << std::endl;
                std::cout << "============================================================================" << std::endl;
                std::cout << " 10^4 sim time\t| Avg trace sim time\t| End-to-end performance" << std::endl;
                std::cout << "----------------------------------------------------------------------------" << std::endl;
        }

        uint i = 0;

        // Check the state space exhaustively
        do
        {
                // Solution has direct pointers to the Tasks in the core...
                if (solution.fitness (Option::verbose1_, true, &temp) > 0.0)
                {
                        if (endtoend_ < temp) endtoend_ = temp;
                        if (verbose)
                        {
                                std::cout << std::endl << std::endl << "System is unschedulable. Execution trace:" << std::endl;
                                system_ptr->reset ();
                                bool verbose = Option::verbose1_;
                                Option::verbose1_ = true;
                                system_ptr->simulate (Option::verbose1_, true);
                                Option::verbose1_ = verbose;

                                time_t end_time;
                                time (&end_time);
                                uint perf = end_time - start_time;
                                std::cout << std::endl << "Analysis complete. System is unschedulable." << std::endl;
                                std::cout << "Analysis time: " << perf << " seconds." << std::endl;
                                std::cout << "Worst case end-to-end performance encountered: " << endtoend_ << std::endl;
                        }

                        return false;
                }

                if (endtoend_ < temp) endtoend_ = temp;

                if (++i == 10000)
                {
                        time_t end_block;
                        time (&end_block);
                        uint block = end_block - start_block;
                        std::cout << " " << block << " secs\t\t| " << std::fixed << std::setprecision (1) << (double)block/10 << " ms\t\t| " << endtoend_ << std::endl;
                        i = 0;
                        time (&start_block);
                }

                system_ptr->reset ();
        }
        while (branching_point (&mc_queue, verbose));

        if (verbose)
        {
                time_t end_time;
                time (&end_time);
                uint perf = end_time - start_time;
                std::cout << "Analysis complete. No errors found." << std::endl;
                std::cout << "Analysis time: " << perf << " seconds." << std::endl;
                std::cout << "Worst case end-to-end performance: " << endtoend_ << std::endl;
        }
        return true;
}
        
};

---