From 8e4e692e7f15d42a7838c8d02e45c92e91a4a312 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 7 Nov 2009 02:56:45 +0100 Subject: [PATCH] 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. --- ChangeLog | 27 +++++++++++++++++++++++++++ src/ltlast/automatop.cc | 7 +++++++ src/ltlast/binop.cc | 7 +++++++ src/ltlast/multop.cc | 35 +++++++++++++++++++++++------------ src/ltlast/unop.cc | 5 +++++ src/ltlvisit/clone.cc | 7 +++---- src/ltlvisit/destroy.cc | 18 ++---------------- 7 files changed, 74 insertions(+), 32 deletions(-) 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)); } } }