From cf6602a3be0efd48c76f3540eb9ace0355bdbbbe Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Mar 2004 15:43:10 +0000 Subject: [PATCH] Move the free_list management into a separate class for reuse. * src/misc/freelist.hh, src/misc/freelist.cc: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and make dump_free_list visible. * src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move all the code into free_list::register_n() and bdd_allocator::extend(), and call the former. (bdd_allocator::release_variables): Move all the code into free_list::release_n() and call it. (bdd_allocator::extend): New method. * src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list; --- ChangeLog | 16 ++++++ src/misc/Makefile.am | 2 + src/misc/bddalloc.cc | 93 ++++++---------------------------- src/misc/bddalloc.hh | 10 ++-- src/misc/freelist.cc | 118 +++++++++++++++++++++++++++++++++++++++++++ src/misc/freelist.hh | 69 +++++++++++++++++++++++++ src/tgba/bdddict.cc | 6 +-- 7 files changed, 228 insertions(+), 86 deletions(-) create mode 100644 src/misc/freelist.cc create mode 100644 src/misc/freelist.hh diff --git a/ChangeLog b/ChangeLog index d8a234e66..1e5d139ad 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2004-03-18 Alexandre Duret-Lutz + + Move the free_list management into a separate class for reuse. + + * src/misc/freelist.hh, src/misc/freelist.cc: New files. + * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. + * src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and + make dump_free_list visible. + * src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move + all the code into free_list::register_n() and + bdd_allocator::extend(), and call the former. + (bdd_allocator::release_variables): Move all the code into + free_list::release_n() and call it. + (bdd_allocator::extend): New method. + * src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list; + 2004-03-09 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0s. diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 3df125c71..2b0253fdb 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -28,6 +28,7 @@ misc_HEADERS = \ bddalloc.hh \ bddlt.hh \ escape.hh \ + freelist.hh \ hash.hh \ minato.hh \ version.hh @@ -36,5 +37,6 @@ noinst_LTLIBRARIES = libmisc.la libmisc_la_SOURCES = \ bddalloc.cc \ escape.cc \ + freelist.cc \ minato.cc \ version.cc diff --git a/src/misc/bddalloc.cc b/src/misc/bddalloc.cc index 2c71bfd37..9ffd54669 100644 --- a/src/misc/bddalloc.cc +++ b/src/misc/bddalloc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -32,7 +32,7 @@ namespace spot : lvarnum(varnum) { initialize(); - free_list.push_front(pos_lenght_pair(0, lvarnum)); + fl.push_front(pos_lenght_pair(0, lvarnum)); } void @@ -71,52 +71,27 @@ namespace spot int bdd_allocator::allocate_variables(int n) { - // Browse the free list until we find N consecutive variables. We - // try not to fragment the list my allocating the variables in the - // smallest free range we find. - free_list_type::iterator best = free_list.end(); - free_list_type::iterator cur; - for (cur = free_list.begin(); cur != free_list.end(); ++cur) - { - if (cur->second < n) - continue; - if (n == cur->second) - { - best = cur; - break; - } - if (best == free_list.end() - || cur->second < best->second) - best = cur; - } + return register_n(n); + } - // We have found enough free variables. - if (best != free_list.end()) - { - int result = best->first; - best->second -= n; - assert(best->second >= 0); - // Erase the range if it's now empty. - if (best->second == 0) - free_list.erase(best); - else - best->first += n; - return result; - } - - // We haven't found enough adjacent free variables; - // ask BuDDy for some more. + void + bdd_allocator::release_variables(int base, int n) + { + release_n(base, n); + } + int + bdd_allocator::extend(int n) + { // If we already have some free variable at the end // of the variable space, allocate just the difference. - if (free_list.size() > 0 - && free_list.back().first + free_list.back().second == lvarnum) + if (fl.size() > 0 && fl.back().first + fl.back().second == lvarnum) { - int res = free_list.back().first; - int endvar = free_list.back().second; + int res = fl.back().first; + int endvar = fl.back().second; assert(n > endvar); extvarnum(n - endvar); - free_list.pop_back(); + fl.pop_back(); return res; } else @@ -127,40 +102,4 @@ namespace spot return res; } } - - void - bdd_allocator::release_variables(int base, int n) - { - free_list_type::iterator cur; - int end = base + n; - for (cur = free_list.begin(); cur != free_list.end(); ++cur) - { - // Append to a range ... - if (cur->first + cur->second == base) - { - cur->second += n; - // Maybe the next item on the list can be merged. - free_list_type::iterator next = cur; - ++next; - if (next != free_list.end() - && next->first == end) - { - cur->second += next->second; - free_list.erase(next); - } - return; - } - // ... or prepend to a range ... - if (cur->first == end) - { - cur->first -= n; - cur->second += n; - return; - } - // ... or insert a new range. - if (cur->first > end) - break; - } - free_list.insert(cur, pos_lenght_pair(base, n)); - } } diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh index 7e4500591..ba3abed98 100644 --- a/src/misc/bddalloc.hh +++ b/src/misc/bddalloc.hh @@ -22,14 +22,14 @@ #ifndef SPOT_MISC_BDDALLOC_HH # define SPOT_MISC_BDDALLOC_HH +#include "freelist.hh" #include #include namespace spot { - /// Manage ranges of variables. - class bdd_allocator + class bdd_allocator: private free_list { public: /// Default constructor. @@ -40,16 +40,16 @@ namespace spot int allocate_variables(int n); /// Release \a n BDD variables starting at \a base. void release_variables(int base, int n); + + using free_list::dump_free_list; protected: static bool initialized; ///< Whether the BDD library has been initialized. static int varnum; ///< number of variables in use in the BDD library. int lvarnum; ///< number of variables in use in this allocator. - typedef std::pair pos_lenght_pair; - typedef std::list free_list_type; - free_list_type free_list; ///< Tracks unused BDD variables. private: /// Require more variables. void extvarnum(int more); + virtual int extend(int n); }; } diff --git a/src/misc/freelist.cc b/src/misc/freelist.cc new file mode 100644 index 000000000..ce2d0bfbb --- /dev/null +++ b/src/misc/freelist.cc @@ -0,0 +1,118 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "freelist.hh" +#include +#include + +namespace spot +{ + + free_list::~free_list() + { + } + + int + free_list::register_n(int n) + { + // Browse the free list until we find N consecutive variables. We + // try not to fragment the list my allocating the variables in the + // smallest free range we find. + free_list_type::iterator best = fl.end(); + free_list_type::iterator cur; + for (cur = fl.begin(); cur != fl.end(); ++cur) + { + if (cur->second < n) + continue; + if (n == cur->second) + { + best = cur; + break; + } + if (best == fl.end() + || cur->second < best->second) + best = cur; + } + + // We have found enough free variables. + if (best != fl.end()) + { + int result = best->first; + best->second -= n; + assert(best->second >= 0); + // Erase the range if it's now empty. + if (best->second == 0) + fl.erase(best); + else + best->first += n; + return result; + } + + // We haven't found enough adjacent free variables; + // ask for some more. + return extend(n); + } + + void + free_list::release_n(int base, int n) + { + free_list_type::iterator cur; + int end = base + n; + for (cur = fl.begin(); cur != fl.end(); ++cur) + { + // Append to a range ... + if (cur->first + cur->second == base) + { + cur->second += n; + // Maybe the next item on the list can be merged. + free_list_type::iterator next = cur; + ++next; + if (next != fl.end() && next->first == end) + { + cur->second += next->second; + fl.erase(next); + } + return; + } + // ... or prepend to a range ... + if (cur->first == end) + { + cur->first -= n; + cur->second += n; + return; + } + // ... or insert a new range. + if (cur->first > end) + break; + } + fl.insert(cur, pos_lenght_pair(base, n)); + } + + std::ostream& + free_list::dump_free_list(std::ostream& os) const + { + free_list_type::const_iterator i; + for (i = fl.begin(); i != fl.end(); ++i) + os << " (" << i->first << ", " << i->second << ")"; + return os; + } + +} diff --git a/src/misc/freelist.hh b/src/misc/freelist.hh new file mode 100644 index 000000000..a6cb7dcb0 --- /dev/null +++ b/src/misc/freelist.hh @@ -0,0 +1,69 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + + +#ifndef SPOT_MISC_FREELIST_HH +# define SPOT_MISC_FREELIST_HH + +#include +#include + +namespace spot +{ + + /// Manage list of free integers. + class free_list + { + public: + virtual ~free_list(); + + /// \brief Find \a n consecutive integers. + /// + /// Browse the list of free integers until \a n consecutive + /// integers are found. Extend the list (using extend()) otherwise. + /// \return the first integer of the range + int register_n(int n); + + /// Release \a n consecutive integers starting at \a base. + void release_n(int base, int n); + + /// Dump the list to \a os for debugging. + std::ostream& dump_free_list(std::ostream& os) const; + protected: + + /// Allocate \a n integer. + /// + /// This function is called by register_n() when the free list is + /// empty or if \a n consecutive integers could not be found. It + /// should allocate more integers, possibly changing the list, and + /// return the first integer on a range of n consecutive integer + /// requested by the user. + virtual int extend(int n) = 0; + + /// Such pairs describe \c second free integer starting at \first. + typedef std::pair pos_lenght_pair; + typedef std::list free_list_type; + free_list_type fl; ///< Tracks unused BDD variables. + }; + +} + +#endif // SPOT_MISC_FREELIST_HH diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 2051d95cc..7b8d10a13 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -269,9 +269,7 @@ namespace spot to_string(fi->first, os) << "]" << std::endl; } os << "Free list:" << std::endl; - free_list_type::const_iterator i; - for (i = free_list.begin(); i != free_list.end(); ++i) - os << " (" << i->first << ", " << i->second << ")"; + dump_free_list(os); os << std::endl; return os; }