From patchwork Mon Jul 19 22:05:29 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Patrick Palka X-Patchwork-Id: 1507306 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=T/rQV/Vr; dkim-atps=neutral Received: from sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 4GTGCG6tq3z9sRN for ; Tue, 20 Jul 2021 08:06:34 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 78B773854804 for ; Mon, 19 Jul 2021 22:06:30 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 78B773854804 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1626732390; bh=B9JUnQCfWBXY0SDUNzruvY9SzjSG5AEMaMTsZb254gE=; h=To:Subject:Date:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:From; b=T/rQV/VroCTPq9yhpKjwViL/Qm2TjFrfI8nMko0IgrXw0N93xLV9ZNqd1GJnIJK11 PSr+ODbDDWj3Li9gTQqa7Gbny7L8Gu/zGEYc/zSwYQ15gpsT15iKPxBu9BqzVy+SyC eA7l33rm3OL55QiZzP96xkpQsrsfPwwKLf1PAGoo= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [216.205.24.124]) by sourceware.org (Postfix) with ESMTP id 37692385800A for ; Mon, 19 Jul 2021 22:05:46 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 37692385800A Received: from mail-qt1-f198.google.com (mail-qt1-f198.google.com [209.85.160.198]) (Using TLS) by relay.mimecast.com with ESMTP id us-mta-89-wxTE0e2uPIWqB-Ie18eoXg-1; Mon, 19 Jul 2021 18:05:39 -0400 X-MC-Unique: wxTE0e2uPIWqB-Ie18eoXg-1 Received: by mail-qt1-f198.google.com with SMTP id l19-20020a05622a1753b0290269bd8044e1so1753159qtk.10 for ; Mon, 19 Jul 2021 15:05:39 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:mime-version :content-transfer-encoding; bh=B9JUnQCfWBXY0SDUNzruvY9SzjSG5AEMaMTsZb254gE=; b=HJ3D90c4dpOKImFHQYZ4kZLwOdVXGUnwRNoV2mxxdLBFcQKH8onxNtgsz2IM2l5n6C GbFO9bemk1I+7O9owoOHa+rS6bs0+cEndSilEJEXAKwmeBJnU/Hdt9wJsqEwTzvjbvuj DAGLRRATyoP83wWW3ilMfX9/EnJ4UxC7WOKglQlk4gsFshHzodln4cEWjNxsDVPey/L9 FAfig3PMek/PC8vt4nn7LYZbznt3NrsdDXsN/xXdgoUBCqhGEICKgvYR7wf0nvxLkpOg XJNYLR1NclMLjIyRruUp02CX5TrPfqG/EqBR6d7uFaSfJxg1ENTKFHF0bpy9PE43TvSa msXw== X-Gm-Message-State: AOAM530VPXAvSM0N8J3xTwE92naqwPNyUBVEaX0vpLBP2MsYD7rMT6EV WltFIAaIVGhYbpSCQO4rhMORiZU+KLaDPnMA+a39tghAl+9dOZ4Hdagfo7z3WlUvjra5CLtAFSH 9RgJhgdefBL1/6NBKG4SItpcZ7pt7g4HfYwDdWF3rcj8p3EaBgWn87yykO7c0iZwR3V8= X-Received: by 2002:ae9:e002:: with SMTP id m2mr26279987qkk.474.1626732339076; Mon, 19 Jul 2021 15:05:39 -0700 (PDT) X-Google-Smtp-Source: ABdhPJyjtkkFpi3g8OYwFFI6G3bn1Cpqp3n4b/X6dvHgQWTiyf4O02cCbAPDgZ5hgd+H088ID76xUg== X-Received: by 2002:ae9:e002:: with SMTP id m2mr26279956qkk.474.1626732338711; Mon, 19 Jul 2021 15:05:38 -0700 (PDT) Received: from localhost.localdomain (ool-457d493a.dyn.optonline.net. [69.125.73.58]) by smtp.gmail.com with ESMTPSA id c6sm1239811qke.133.2021.07.19.15.05.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 19 Jul 2021 15:05:38 -0700 (PDT) To: gcc-patches@gcc.gnu.org Subject: [PATCH] c++: Improve memory usage of subsumption [PR100828] Date: Mon, 19 Jul 2021 18:05:29 -0400 Message-Id: <20210719220529.2446563-1-ppalka@redhat.com> X-Mailer: git-send-email 2.32.0.264.g75ae10bc75 MIME-Version: 1.0 X-Mimecast-Spam-Score: 0 X-Mimecast-Originator: redhat.com X-Spam-Status: No, score=-16.5 required=5.0 tests=BAYES_00, DKIMWL_WL_HIGH, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_LOW, RCVD_IN_MSPIKE_H4, RCVD_IN_MSPIKE_WL, SPF_HELO_NONE, SPF_NONE, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Patrick Palka via Gcc-patches From: Patrick Palka Reply-To: Patrick Palka Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" 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? 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 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);