IFInterpreter.cpp

Go to the documentation of this file.

/** @file IFInterpreter.cpp
* @author Gabor Madl
* @date Created 11/2005
* @brief This interpreter generates input for the IF toolset from the DREAM models.
*
*
* =================================================================
* 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 "IFInterpreter.h"

namespace DREAM
{

IFInterpreter::IFInterpreter (DREAM::System* system_ptr)
: system_ptr_ (system_ptr)
{
}

IFInterpreter::~IFInterpreter ()
{
}

std::string IFInterpreter::create_fixedpriority_exec_assignment (NODE_MAP* node_map, std::string scheduler_id, const DREAM::Node* const node)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        uint k = 0;
        NODE_MAP::const_iterator node_iter;
        std::string output = "\t\t task ({common}0).exec[";

        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if ((node_iter->first) == node->id ())
                {
                        output << k << "] := true;\n";
                }
                ++k;
        }

        k = 0;
        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if (node_iter->second->scheduler ()->id () == scheduler_id)
                {
                        if (node_iter->second->priority () > node->priority ())
                        {       
                                output << "\t\t task ({common}0).exec[" << k << "] := false;\n";
                        }
                }
                ++k;
        }

        return output;
}

std::string IFInterpreter::create_fixedpriority_guard (NODE_MAP* node_map, std::string scheduler_id, const DREAM::Node* const node)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        uint k = 0;
        NODE_MAP::const_iterator node_iter;
        std::string output = " ({common}0).en[";

        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if ((node_iter->first) == node->id ())
                {
                                output << k << "]";
                }
                ++k;
        }

        k = 0;
        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if (node_iter->second->scheduler ()->id () == scheduler_id)
                {
                        if (node_iter->second->priority () <= node->priority ())
                                if ((node_iter->second->priority () < node->priority ()) ||
                                                 (node_iter->second->subpriority () < node->subpriority ()))
                                {       
                                        output << " and (({common}0).en[" << k << "] = false)";
                                }
                }
                ++k;
        }

        return output;
}

std::string IFInterpreter::create_fixedpriority_back_guard (NODE_MAP* node_map, std::string scheduler_id, const DREAM::Node* const node)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        NODE_MAP::const_iterator node_iter;
        std::string output;

        uint k = 0, f = 0;
        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if (node_iter->second->scheduler ()->id () == scheduler_id)
                {
                        if (node_iter->second->priority () == node->priority ())
                        {
                                if (node_iter->second->subpriority () < node->subpriority ())
                                {       
                                        if (f != 0)
                                                output << " or ({common}0).en[" << k << "]";
                                        else
                                        {
                                                output << " ({common}0).en[" << k << "]";
                                                f = 1;
                                        }
                                }
                        }
                }
                ++k;
        }

        return output;
}

std::string IFInterpreter::create_fixedpriority_preemption_guard (NODE_MAP* node_map, std::string scheduler_id, const DREAM::Node* const node)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        NODE_MAP::const_iterator node_iter;
        std::string output;

        uint k = 0, f= 0;
        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if (node_iter->second->scheduler ()->id () == scheduler_id)
                {
                        if (node_iter->second->priority () < node->priority ())
                        {
                                if (f != 0)
                                        output << " or ({common}0).en[" << k << "]";
                                else
                                {
                                        output << " ({common}0).en[" << k << "]";
                                        f = 1;
                                }
                        }
                }
                ++k;
        }

        return output;
}

bool IFInterpreter::highestpriority (DREAM::Node* node_ptr)
{
        return node_ptr->scheduler ()->highestpriority (node_ptr);
}

bool IFInterpreter::lowestpriority (DREAM::Node* node_ptr)
{
        return node_ptr->scheduler ()->lowestpriority (node_ptr);
}

void IFInterpreter::visitor_if (char* outputFile)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        std::cout << "\nGenerating Verimag IF toolset input \"" << outputFile << "\"...\n\n";

        std::ofstream f_stream (outputFile, std::ios::trunc);

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

        f_stream << "system dre;\n\nsignal event ();\n\n/*\n * Type declarations\n *\n */\n" << std::endl;

        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);

        f_stream << "const pr=1;\nconst NTASKS=" << task_map.size () << ";\ntype flags=array[NTASKS] of boolean;\n" << std::endl;

        DREAM::NODE_MAP::const_iterator node_iter;
        uint i = 0;

        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                f_stream << "const dl" << i << "=" << node_iter->second->deadline () << ";\n";
                ++i;
        }

        f_stream << std::endl;
        i = 0;

        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                f_stream << "const wcet" << i << "=" << node_iter->second->wcet () << ";\n";
                ++i;
        }

        f_stream << std::endl;
        i = 0;

        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                f_stream << "const bcet" << i << "=" << node_iter->second->bcet () << ";\n";
                ++i;
        }

        f_stream << "\n/*\n * Signalroutes\n *\n *\n"
                << " * Use signalroutes only if you have to model lossy channels\n"
                << " * or channels with delays. The IF message passing builds on\n"
                << " * a buffered FIFO by default therefore it is suitable to\n"
                << " * model the real-time event channel mechanism as implemented\n"
                << " * in several middleware. Try to avoid signalroutes as they\n"
                << " * tend to agressively increase the state space size.\n *\n *\n";

        const DREAM::NODE_MAP* node_map;
        DREAM::NODE_MAP::const_iterator node_iter2;

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

                for (node_iter2 = node_map->begin (); node_iter2 != node_map->end (); node_iter2++)
                {
                        if (node_iter->second->get_source (&task_map, &channel_map, &timer_map) != NULL)
                        {
                                if (node_iter->second->wcet () != 0)
                                {
                                        f_stream << " */\nsignalroute " << node_iter->first << " (1) #fifo #reliable #unicast #delay["
                                                << node_iter->second->bcet () << "," << node_iter->second->wcet () << "];\n"
                                                << "\tfrom task_" << node_iter->second->get_source (&task_map, &channel_map, &timer_map)->id ()
                                                << " to task_" << node_iter2->first << "\n\twith event;\n/*" << std::endl;
                                }
                                else
                                {
                                        f_stream << " * signalroute " << node_iter->first << " (1) #fifo #reliable #unicast #urgent;\n"
                                                << " *\tfrom task_" << node_iter->second->get_source (&task_map, &channel_map, &timer_map)->id ()
                                                << " to task_" << node_iter2->first << "\n *\twith event;\n *" << std::endl;
                                }
                        }

                        ++i;
                }
        }

        f_stream << "*/\n\n/*\n * Common variables\n *\n * We need a separate process to store them...\n */\n" << std::endl;

        f_stream << "process common (1);\n\nvar en flags public;\nvar exec flags public;\n\nendprocess;\n" << std::endl;

        system_ptr_->visitor_if (&task_map, &channel_map, &timer_map, f_stream);

        // Generate the schedulers
        SCHEDULER_MAP::const_iterator scheduler_iter;
        const SCHEDULER_MAP* scheduler_map = system_ptr_->scheduler_map ();

        for (scheduler_iter = scheduler_map->begin (); scheduler_iter != scheduler_map->end (); scheduler_iter++)
        {
                if (scheduler_iter->second->CPUs () > 0)
                {
                        // Generate idle and select states
                        f_stream << "/*\n * Fixed-priority scheduler\n * \n */\n\nprocess scheduler_" << scheduler_iter->first
                                << " (1);\n\nstate start #start ;\n\tdeadline eager;\n\tnextstate initial;\n"
                                << "endstate;\n\n/* Scheduling enabled tasks */\n\nstate initial;\n\tdeadline eager;\n";

                        i = 0;
                        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
                        {
                                // Check whether task belongs to scheduler
                                if (node_iter->second->scheduler ()->id () == scheduler_iter->first)
                                {
                                        f_stream << "\tprovided " << create_fixedpriority_guard (&task_map, scheduler_iter->first, node_iter->second) << ";\n"
                                                << create_fixedpriority_exec_assignment (&task_map, scheduler_iter->first, node_iter->second)
                                                << "\t\t\tnextstate schedule_" << node_iter->first << ";\n" << std::endl;
                                }

                                ++i;
                        }

                        f_stream << "endstate;\n\n";

                        i = 0;
                        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
                        {
                                // Check whether task belongs to scheduler
                                if (node_iter->second->scheduler ()->id () == scheduler_iter->first)
                                {
                                        f_stream << "state schedule_" << node_iter->first << ";" << std::endl;
                                        
                                        std::string message = 
                                                create_fixedpriority_back_guard (&task_map, scheduler_iter->first, node_iter->second);
                                        if (!message.empty ())
                                        {
                                                f_stream << "\tdeadline eager;\n"
                                                        << "\t/*\n\t * We have to hack the scheduler to compensate for\n"
                                                        << "\t * the race conditions caused by non-atomic broadcasts...\n\t *\n\t */" << std::endl;

                                                if ((node_iter->second->scheduler ()->nonpreemptive ())||
                                                         (node_iter->second->scheduler ()->highestpriority (node_iter->second)))
                                                {
                                                        // Non-preemptive task
                                                        f_stream << "\tprovided " << message << ";\n"
                                                                << "\twhen ({task_" << node_iter->first << "}0).ce = 0;\n"
                                                                << "\t\ttask ({common}0).exec[" << i << "] := false;\n\t\t\tnextstate initial;" << std::endl;
                                                }
                                                else
                                                {
                                                        // Preemptive task non-preemptive stop
                                                        f_stream << "\tprovided (" << message << ") and ({task_" << node_iter->first << "}0).et = 0;\n"
                                                                << "\twhen ({task_" << node_iter->first << "}0).ce = 0;\n" //
                                                                << "\t\ttask ({common}0).exec[" << i << "] := false;\n\t\t\tnextstate initial;" << std::endl;
                                                }
                                        }

                                        // Preemptions
                                        message = create_fixedpriority_preemption_guard (&task_map, scheduler_iter->first, node_iter->second);

                                        if (!message.empty ())
                                        {
                                                f_stream << "\t/* Preemptions */\n\tprovided " << message << ";\n"
                                                        << "\t\ttask ({common}0).exec[" << i << "] := false;\n\t\t\tnextstate initial;" << std::endl;
                                        }

                                        f_stream << "\tprovided ({common}0).en[" << i << "] = false;\n"
                                                << "\t\ttask ({common}0).exec[" << i << "] := false;\n\t\t\tnextstate initial;\n\nendstate;\n" << std::endl;
                                }

                                ++i;
                        }

                        f_stream << "endprocess;\n" << std::endl;
                }
        }

        // Observer
        f_stream << "endsystem;\n\n/*\n * Observer\n *\n */\n\npure observer safety;\n\nstate idle #start ;\n\tdeadline eager;\n" << std::endl;

        i = 0;
        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                if ((node_iter->second->scheduler ()->nonpreemptive ())||
                         (node_iter->second->scheduler ()->highestpriority (node_iter->second)))
                {
                        // Non-preemptive task
                        f_stream << "\tprovided ({task_" << node_iter->first << "}0) instate wait;\n"
                                << "\twhen ({task_" << node_iter->first << "}0).cd >= dl" << i << ";\n\t\tnextstate error;\n"
                                << "\tprovided ({task_" << node_iter->first << "}0) instate run;\n"
                                << "\twhen ({task_" << node_iter->first << "}0).cd >= dl" << i << ";\n\t\tnextstate error;\n" << std::endl;
                }
                else
                {
                        // Preemptive task
                        f_stream << "\tprovided ({task_" << node_iter->first << "}0) instate wait;\n"
                                << "\twhen ({task_" << node_iter->first << "}0).cd >= dl" << i << " - ({task_" << node_iter->first << "}0).pre;\n\t\tnextstate error;\n"
                                << "\tprovided ({task_" << node_iter->first << "}0) instate run;\n"
                                << "\twhen ({task_" << node_iter->first << "}0).cd >= dl" << i << " - ({task_" << node_iter->first << "}0).pre;\n\t\tnextstate error;\n" << std::endl;
                }

                ++i;
        }

        f_stream << "endstate;\n\nstate error #error ;\nendstate;\n\nendobserver;" << std::endl;

        f_stream.close ();
}

};

---