From: Jason Merrill <jason@redhat.com>
To: Patrick Palka <ppalka@redhat.com>
Cc: GCC Patches <gcc-patches@gcc.gnu.org>
Subject: Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]
Date: Wed, 11 Aug 2021 09:46:05 -0400 [thread overview]
Message-ID: <e945013d-d36e-be92-7fcb-1b6bce928287@redhat.com> (raw)
In-Reply-To: <CAMOnLZZMQGjfF3ynHzCX98=N2kS_Ui1nD8rnRegRGiu_C2dEVg@mail.gmail.com>
On 8/9/21 5:07 PM, Patrick Palka wrote:
> On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <jason@redhat.com> wrote:
>>
>> On 7/19/21 6:05 PM, Patrick Palka wrote:
>>> Constraint subsumption is implemented in two steps. The first step
>>> computes the disjunctive (or conjunctive) normal form of one of the
>>> constraints, and the second step verifies that each clause in the
>>> decomposed form implies the other constraint. Performing these two
>>> steps separately is problematic because in the first step the
>>> disjunctive normal form can be exponentially larger than the original
>>> constraint, and by computing it ahead of time we'd have to keep all of
>>> it in memory.
>>>
>>> This patch fixes this exponential blowup in memory usage by interleaving
>>> these two steps, so that as soon as we decompose one clause we check
>>> implication for it. In turn, memory usage during subsumption is now
>>> worst case linear in the size of the constraints rather than
>>> exponential, and so we can safely remove the hard limit of 16 clauses
>>> without introducing runaway memory usage on some inputs. (Note the
>>> _time_ complexity of subsumption is still exponential in the worst case.)
>>>
>>> In order for this to work we need formula::branch to prepend the copy
>>> of the current clause directly after the current clause rather than
>>> at the end of the list, so that we fully decompose a clause shortly
>>> after creating it. Otherwise we'd end up accumulating exponentially
>>> many (partially decomposed) clauses in memory anyway.
>>>
>>> Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
>>> range-v3 and cmcstl2. Does this look OK for trunk and perhaps 11?
>>
>> OK for trunk.
>
> Thanks a lot, patch committed to trunk as r12-2658. Since this low
> complexity limit was introduced in GCC 10, what do you think about
> increasing the limit from 16 to say 128 in the 10/11 release branches
> as a relatively safe stopgap?
Now that 11.2 is out, go ahead and apply this patch to the 11 branch.
Won't a limit of 128 in GCC 10 lead to extremely long compile times for
affected code? Is that more desirable than an error?
>>> PR c++/100828
>>>
>>> gcc/cp/ChangeLog:
>>>
>>> * logic.cc (formula::formula): Use emplace_back.
>>> (formula::branch): Insert a copy of m_current in front of
>>> m_current instead of at the end of the list.
>>> (formula::erase): Define.
>>> (decompose_formula): Remove.
>>> (decompose_antecedents): Remove.
>>> (decompose_consequents): Remove.
>>> (derive_proofs): Remove.
>>> (max_problem_size): Remove.
>>> (diagnose_constraint_size): Remove.
>>> (subsumes_constraints_nonnull): Rewrite directly in terms of
>>> decompose_clause and derive_proof, interleaving decomposition
>>> with implication checking. Use formula::erase to free the
>>> current clause before moving on to the next one.
>>> ---
>>> gcc/cp/logic.cc | 118 ++++++++++++++----------------------------------
>>> 1 file changed, 35 insertions(+), 83 deletions(-)
>>>
>>> diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
>>> index 142457e408a..3f872c11fe2 100644
>>> --- a/gcc/cp/logic.cc
>>> +++ b/gcc/cp/logic.cc
>>> @@ -223,9 +223,7 @@ struct formula
>>>
>>> formula (tree t)
>>> {
>>> - /* This should call emplace_back(). There's an extra copy being
>>> - invoked by using push_back(). */
>>> - m_clauses.push_back (t);
>>> + m_clauses.emplace_back (t);
>>> m_current = m_clauses.begin ();
>>> }
>>>
>>> @@ -248,8 +246,7 @@ struct formula
>>> clause& branch ()
>>> {
>>> gcc_assert (!done ());
>>> - m_clauses.push_back (*m_current);
>>> - return m_clauses.back ();
>>> + return *m_clauses.insert (std::next (m_current), *m_current);
>>> }
>>>
>>> /* Returns the position of the current clause. */
>>> @@ -287,6 +284,14 @@ struct formula
>>> return m_clauses.end ();
>>> }
>>>
>>> + /* Remove the specified clause. */
>>> +
>>> + void erase (iterator i)
>>> + {
>>> + gcc_assert (i != m_current);
>>> + m_clauses.erase (i);
>>> + }
>>> +
>>> std::list<clause> m_clauses; /* The list of clauses. */
>>> iterator m_current; /* The current clause. */
>>> };
>>> @@ -659,39 +664,6 @@ decompose_clause (formula& f, clause& c, rules r)
>>> f.advance ();
>>> }
>>>
>>> -/* Decompose the logical formula F according to the logical
>>> - rules determined by R. The result is a formula containing
>>> - clauses that contain only atomic terms. */
>>> -
>>> -void
>>> -decompose_formula (formula& f, rules r)
>>> -{
>>> - while (!f.done ())
>>> - decompose_clause (f, *f.current (), r);
>>> -}
>>> -
>>> -/* Fully decomposing T into a list of sequents, each comprised of
>>> - a list of atomic constraints, as if T were an antecedent. */
>>> -
>>> -static formula
>>> -decompose_antecedents (tree t)
>>> -{
>>> - formula f (t);
>>> - decompose_formula (f, left);
>>> - return f;
>>> -}
>>> -
>>> -/* Fully decomposing T into a list of sequents, each comprised of
>>> - a list of atomic constraints, as if T were a consequent. */
>>> -
>>> -static formula
>>> -decompose_consequents (tree t)
>>> -{
>>> - formula f (t);
>>> - decompose_formula (f, right);
>>> - return f;
>>> -}
>>> -
>>> static bool derive_proof (clause&, tree, rules);
>>>
>>> /* Derive a proof of both operands of T. */
>>> @@ -744,28 +716,6 @@ derive_proof (clause& c, tree t, rules r)
>>> }
>>> }
>>>
>>> -/* Derive a proof of T from disjunctive clauses in F. */
>>> -
>>> -static bool
>>> -derive_proofs (formula& f, tree t, rules r)
>>> -{
>>> - for (formula::iterator i = f.begin(); i != f.end(); ++i)
>>> - if (!derive_proof (*i, t, r))
>>> - return false;
>>> - return true;
>>> -}
>>> -
>>> -/* The largest number of clauses in CNF or DNF we accept as input
>>> - for subsumption. This an upper bound of 2^16 expressions. */
>>> -static int max_problem_size = 16;
>>> -
>>> -static inline bool
>>> -diagnose_constraint_size (tree t)
>>> -{
>>> - error_at (input_location, "%qE exceeds the maximum constraint complexity", t);
>>> - return false;
>>> -}
>>> -
>>> /* Key/value pair for caching subsumption results. This associates a pair of
>>> constraints with a boolean value indicating the result. */
>>>
>>> @@ -845,31 +795,33 @@ subsumes_constraints_nonnull (tree lhs, tree rhs)
>>> if (bool *b = lookup_subsumption(lhs, rhs))
>>> return *b;
>>>
>>> - int n1 = dnf_size (lhs);
>>> - int n2 = cnf_size (rhs);
>>> -
>>> - /* Make sure we haven't exceeded the largest acceptable problem. */
>>> - if (std::min (n1, n2) >= max_problem_size)
>>> - {
>>> - if (n1 < n2)
>>> - diagnose_constraint_size (lhs);
>>> - else
>>> - diagnose_constraint_size (rhs);
>>> - return false;
>>> - }
>>> -
>>> - /* Decompose the smaller of the two formulas, and recursively
>>> - check for implication of the larger. */
>>> - bool result;
>>> - if (n1 <= n2)
>>> - {
>>> - formula dnf = decompose_antecedents (lhs);
>>> - result = derive_proofs (dnf, rhs, left);
>>> - }
>>> + tree x, y;
>>> + rules r;
>>> + if (dnf_size (lhs) <= cnf_size (rhs))
>>> + /* When LHS looks simpler than RHS, we'll determine subsumption by
>>> + decomposing LHS into its disjunctive normal form and checking that
>>> + each (conjunctive) clause implies RHS. */
>>> + x = lhs, y = rhs, r = left;
>>> else
>>> + /* Otherwise, we'll determine subsumption by decomposing RHS into its
>>> + conjunctive normal form and checking that each (disjunctive) clause
>>> + implies LHS. */
>>> + x = rhs, y = lhs, r = right;
>>> +
>>> + /* Decompose X into a list of sequents according to R, and recursively
>>> + check for implication of Y. */
>>> + bool result = true;
>>> + formula f (x);
>>> + while (!f.done ())
>>> {
>>> - formula cnf = decompose_consequents (rhs);
>>> - result = derive_proofs (cnf, lhs, right);
>>> + auto i = f.current ();
>>> + decompose_clause (f, *i, r);
>>> + if (!derive_proof (*i, y, r))
>>> + {
>>> + result = false;
>>> + break;
>>> + }
>>> + f.erase (i);
>>> }
>>>
>>> return save_subsumption (lhs, rhs, result);
>>>
>>
>
next prev parent reply other threads:[~2021-08-11 13:46 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-07-19 22:05 Patrick Palka
2021-07-19 22:13 ` Patrick Palka
2021-07-28 20:42 ` Jason Merrill
2021-08-09 21:07 ` Patrick Palka
2021-08-11 13:46 ` Jason Merrill [this message]
2021-08-11 14:53 ` Patrick Palka
2021-08-11 17:41 ` Jason Merrill
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=e945013d-d36e-be92-7fcb-1b6bce928287@redhat.com \
--to=jason@redhat.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=ppalka@redhat.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).