diff --git a/ChangeLog b/ChangeLog index ed8bae91f..9d72804e2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,30 @@ +2009-11-07 Alexandre Duret-Lutz + + Change the way references are counted to speedup cloning. + + Before this patch, every time you cloned a formula, the clone + visitor would recurse into the entire AST to increment the + reference count of all nodes. When running ltl2tgba_fm on + the formula generated by "LTLcounterLinear.pl 8", approx 27% of + the time was spent in the clone visitor. + + After this patch, cloning a formula is just an increment of the + reference count of the top node. Children are decremented only + when the top node's ref count is decremented to zero. With this + change, clone() and destroy() become constant time, the + ltl2tgba_fm spend only 0.01% of the time cloning formulae. + + + * src/ltlast/automatop.cc (~automatop): Decrement children. + (instance): Decrement children if the instance already exists. + * src/ltlast/binop.cc, src/ltlast/multop.cc, src/ltlast/unop.cc: + Likewise. + * src/ltlvisit/clone.cc (clone): Simplify, now we only need to + call ref(). + * src/ltlvisit/destroy.cc (destroy): Simplify, now we only need + to call unref(). + (destroy_visitor): Remove, no longer needed. + 2009-11-07 Alexandre Duret-Lutz Make it easier to debug reference counts in LTL nodes. diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index f5b8b8c5e..0c222417b 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -48,6 +48,10 @@ namespace spot assert (i != instances.end()); instances.erase(i); + // Dereference children. + for (unsigned n = 0; n < size(); ++n) + formula::unref(nth(n)); + delete children_; } @@ -73,6 +77,9 @@ namespace spot map::iterator i = instances.find(p); if (i != instances.end()) { + // The instance already exists. + for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) + formula::unref(*vi); delete v; return static_cast(i->second->ref()); } diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 04692d726..af5758402 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -46,6 +46,10 @@ namespace spot map::iterator i = instances.find(p); assert (i != instances.end()); instances.erase(i); + + // Dereference children. + formula::unref(first()); + formula::unref(second()); } void @@ -138,6 +142,9 @@ namespace spot map::iterator i = instances.find(p); if (i != instances.end()) { + // This instance already exists. + formula::unref(first); + formula::unref(second); return static_cast(i->second->ref()); } binop* ap = new binop(op, first, second); diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 47363cced..8317e6fcf 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -26,7 +26,6 @@ #include "multop.hh" #include "constant.hh" #include "visitor.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -54,6 +53,10 @@ namespace spot assert (i != instances.end()); instances.erase(i); + // Dereference children. + for (unsigned n = 0; n < size(); ++n) + formula::unref(nth(n)); + delete children_; } @@ -113,9 +116,10 @@ namespace spot formula* multop::instance(type op, vec* v) { - pair p(op, v); - // Inline children of same kind. + // + // When we construct a formula such as Multop(Op,X,Multop(Op,Y,Z)) + // we will want to inline it as Multop(Op,X,Y,Z). { vec inlined; vec::iterator i = v->begin(); @@ -126,10 +130,7 @@ namespace spot { unsigned ps = p->size(); for (unsigned n = 0; n < ps; ++n) - inlined.push_back(p->nth(n)); - // That sub-formula is now useless, drop it. - // Note that we use unref(), not destroy(), because we've - // adopted its children and don't want to destroy these. + inlined.push_back(p->nth(n)->ref()); formula::unref(*i); i = v->erase(i); } @@ -144,7 +145,7 @@ namespace spot std::sort(v->begin(), v->end(), formula_ptr_less_than()); // Remove duplicates. We can't use std::unique(), because we - // must destroy() any formula we drop. + // must unref() any formula we drop. { formula* last = 0; vec::iterator i = v->begin(); @@ -152,7 +153,7 @@ namespace spot { if (*i == last) { - destroy(*i); + formula::unref(*i); i = v->erase(i); } else @@ -160,7 +161,7 @@ namespace spot last = *i++; } } - } + } vec::size_type s = v->size(); if (s == 0) @@ -178,21 +179,31 @@ namespace spot } else if (s == 1) { + // Simply replace Multop(Op,X) by X. formula* res = (*v)[0]; delete v; return res; } + // The hash key. + pair p(op, v); + map::iterator i = instances.find(p); if (i != instances.end()) { + // The instance already exists. + for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) + formula::unref(*vi); delete v; return static_cast(i->second->ref()); } + + // This is the first instance of this formula. + + // Record the instance in the map, multop* ap = new multop(op, v); instances[p] = ap; - return static_cast(ap->ref()); - + return ap->ref(); } formula* diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 17846baee..963e8484c 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -44,6 +44,9 @@ namespace spot map::iterator i = instances.find(p); assert (i != instances.end()); instances.erase(i); + + // Dereference child. + formula::unref(child()); } void @@ -106,6 +109,8 @@ namespace spot map::iterator i = instances.find(p); if (i != instances.end()) { + // This instance already exists. + formula::unref(child); return static_cast(i->second->ref()); } unop* ap = new unop(op, child); diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 14415ed4d..e08de2c0f 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -93,9 +93,8 @@ namespace spot formula* clone(const formula* f) { - clone_visitor v; - const_cast(f)->accept(v); - return v.result(); + formula* res = const_cast(f)->ref(); + return res; } } } diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 131136d42..9e6e01257 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -25,24 +25,10 @@ namespace spot { namespace ltl { - namespace - { - class destroy_visitor: public postfix_visitor - { - public: - virtual void - doit_default(formula* c) - { - formula::unref(c); - } - }; - } - void destroy(const formula* f) { - destroy_visitor v; - const_cast(f)->accept(v); + formula::unref(const_cast(f)); } } }