From patchwork Sun May 17 19:57:22 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Andrii Nakryiko X-Patchwork-Id: 219084 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org X-Spam-Level: X-Spam-Status: No, score=-9.9 required=3.0 tests=DKIMWL_WL_HIGH, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, HEADER_FROM_DIFFERENT_DOMAINS, INCLUDES_PATCH, MAILING_LIST_MULTI, SIGNED_OFF_BY, SPF_HELO_NONE, SPF_PASS, USER_AGENT_GIT autolearn=ham autolearn_force=no version=3.4.0 Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 31951C433E1 for ; Sun, 17 May 2020 19:57:48 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 0D76520758 for ; Sun, 17 May 2020 19:57:48 +0000 (UTC) Authentication-Results: mail.kernel.org; dkim=pass (1024-bit key) header.d=fb.com header.i=@fb.com header.b="ZGN3upZe" Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1726550AbgEQT5r (ORCPT ); Sun, 17 May 2020 15:57:47 -0400 Received: from mx0a-00082601.pphosted.com ([67.231.145.42]:17210 "EHLO mx0a-00082601.pphosted.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726269AbgEQT5q (ORCPT ); Sun, 17 May 2020 15:57:46 -0400 Received: from pps.filterd (m0044010.ppops.net [127.0.0.1]) by mx0a-00082601.pphosted.com (8.16.0.42/8.16.0.42) with SMTP id 04HJtSMS020898 for ; Sun, 17 May 2020 12:57:45 -0700 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fb.com; h=from : to : cc : subject : date : message-id : in-reply-to : references : mime-version : content-transfer-encoding : content-type; s=facebook; bh=HisIGKAv4VrnMJx7LxmQhcH6r5aSNlVCdz642a7/snU=; b=ZGN3upZesJEg1pHFQ2+tB1eULEOu5b7hI7sViyLuSSNuV4bRYSlDsuoxU5z3F9gqiXb2 VjtRZObJqvUW+09v1jywK5nf1l36/0mURxw5Tar2xSmAk0ANQ6pSRkW6HUunuEjuDEmF S/GLVjhJAI0wRyJvITvvPx8vaBVIN4nc3+k= Received: from maileast.thefacebook.com ([163.114.130.16]) by mx0a-00082601.pphosted.com with ESMTP id 3130134eyx-2 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Sun, 17 May 2020 12:57:45 -0700 Received: from intmgw005.03.ash8.facebook.com (2620:10d:c0a8:1b::d) by mail.thefacebook.com (2620:10d:c0a8:83::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1847.3; Sun, 17 May 2020 12:57:44 -0700 Received: by devbig012.ftw2.facebook.com (Postfix, from userid 137359) id 7B7FB2EC32DC; Sun, 17 May 2020 12:57:39 -0700 (PDT) Smtp-Origin-Hostprefix: devbig From: Andrii Nakryiko Smtp-Origin-Hostname: devbig012.ftw2.facebook.com To: , , , CC: , , Andrii Nakryiko , "Paul E . McKenney" , Jonathan Lemon Smtp-Origin-Cluster: ftw2c04 Subject: [PATCH v2 bpf-next 2/7] tools/memory-model: add BPF ringbuf MPSC litmus tests Date: Sun, 17 May 2020 12:57:22 -0700 Message-ID: <20200517195727.279322-3-andriin@fb.com> X-Mailer: git-send-email 2.24.1 In-Reply-To: <20200517195727.279322-1-andriin@fb.com> References: <20200517195727.279322-1-andriin@fb.com> MIME-Version: 1.0 X-FB-Internal: Safe X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.216, 18.0.676 definitions=2020-05-17_07:2020-05-15,2020-05-17 signatures=0 X-Proofpoint-Spam-Details: rule=fb_default_notspam policy=fb_default score=0 bulkscore=0 phishscore=0 priorityscore=1501 suspectscore=8 lowpriorityscore=0 spamscore=0 adultscore=0 clxscore=1015 impostorscore=0 mlxscore=0 malwarescore=0 mlxlogscore=387 cotscore=-2147483648 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2004280000 definitions=main-2005170182 X-FB-Internal: deliver Sender: netdev-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: netdev@vger.kernel.org Add 4 litmus tests for BPF ringbuf implementation, divided into two different use cases. First, two unbounded case, one with 1 producer and another with 2 producers, single consumer. All reservations are supposed to succeed. Second, bounded case with only 1 record allowed in ring buffer at any given time. Here failures to reserve space are expected. Again, 1- and 2- producer cases, single consumer, are validated. Just for the fun of it, I also wrote a 3-producer cases, it took *16 hours* to validate, but came back successful as well. I'm not including it in this patch, because it's not practical to run it. See output for all included 4 cases and one 3-producer one with bounded use case. Each litmust test implements producer/consumer protocol for BPF ring buffer implementation found in kernel/bpf/ringbuf.c. Due to limitations, all records are assumed equal-sized and producer/consumer counters are incremented by 1. This doesn't change the correctness of the algorithm, though. Verification results: /* 1p1c bounded case */ $ herd7 -unroll 0 -conf linux-kernel.cfg litmus-tests/mpsc-rb+1p1c+bounded.litmus Test mpsc-rb+1p1c+bounded Allowed States 2 0:rFail=0; 1:rFail=0; cx=0; dropped=0; len1=1; px=1; 0:rFail=0; 1:rFail=0; cx=1; dropped=0; len1=1; px=1; Ok Witnesses Positive: 3 Negative: 0 Condition exists (0:rFail=0 /\ 1:rFail=0 /\ dropped=0 /\ px=1 /\ len1=1 /\ (cx=0 \/ cx=1)) Observation mpsc-rb+1p1c+bounded Always 3 0 Time mpsc-rb+1p1c+bounded 0.03 Hash=5bdad0f41557a641370e7fa6b8eb2f43 /* 2p1c bounded case */ $ herd7 -unroll 0 -conf linux-kernel.cfg litmus-tests/mpsc-rb+2p1c+bounded.litmus Test mpsc-rb+2p1c+bounded Allowed States 4 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=0; dropped=1; len1=1; px=1; 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=1; dropped=0; len1=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=1; dropped=1; len1=1; px=1; 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=2; dropped=0; len1=1; px=2; Ok Witnesses Positive: 22 Negative: 0 Condition exists (0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 /\ len1=1 /\ (dropped=0 /\ px=2 /\ (cx=1 \/ cx=2) \/ dropped=1 /\ px=1 /\ (cx=0 \/ cx=1))) Observation mpsc-rb+2p1c+bounded Always 22 0 Time mpsc-rb+2p1c+bounded 119.38 Hash=e2f8f442a02bf7d8c2988ba82cf002d2 /* 1p1c unbounded case */ $ herd7 -unroll 0 -conf linux-kernel.cfg litmus-tests/mpsc-rb+1p1c+unbound.litmus Test mpsc-rb+1p1c+unbound Allowed States 2 0:rFail=0; 1:rFail=0; cx=0; len1=1; px=1; 0:rFail=0; 1:rFail=0; cx=1; len1=1; px=1; Ok Witnesses Positive: 3 Negative: 0 Condition exists (0:rFail=0 /\ 1:rFail=0 /\ px=1 /\ len1=1 /\ (cx=0 \/ cx=1)) Observation mpsc-rb+1p1c+unbound Always 3 0 Time mpsc-rb+1p1c+unbound 0.02 Hash=be9de6487d8e27c3d37802d122e4a87c /* 2p1c unbounded case */ $ herd7 -unroll 0 -conf linux-kernel.cfg litmus-tests/mpsc-rb+2p1c+unbound.litmus Test mpsc-rb+2p1c+unbound Allowed States 3 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=0; len1=1; len2=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=1; len1=1; len2=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; cx=2; len1=1; len2=1; px=2; Ok Witnesses Positive: 42 Negative: 0 Condition exists (0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 /\ px=2 /\ len1=1 /\ len2=1 /\ (cx=0 \/ cx=1 \/ cx=2)) Observation mpsc-rb+2p1c+unbound Always 42 0 Time mpsc-rb+2p1c+unbound 39.19 Hash=f0352aba9bdc03dd0b1def7d0c4956fa /* 3p1c bounded case */ $ herd7 -unroll 0 -conf linux-kernel.cfg mpsc-rb+3p1c+bounded.litmus Test mpsc+ringbuf-spinlock Allowed States 5 0:rFail=0; 1:rFail=0; 2:rFail=0; 3:rFail=0; cx=0; len1=1; len2=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; 3:rFail=0; cx=1; len1=1; len2=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; 3:rFail=0; cx=1; len1=1; len2=1; px=3; 0:rFail=0; 1:rFail=0; 2:rFail=0; 3:rFail=0; cx=2; len1=1; len2=1; px=2; 0:rFail=0; 1:rFail=0; 2:rFail=0; 3:rFail=0; cx=2; len1=1; len2=1; px=3; Ok Witnesses Positive: 558 Negative: 0 Condition exists (0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 /\ 3:rFail=0 /\ len1=1 /\ len2=1 /\ (px=2 /\ (cx=0 \/ cx=1 \/ cx=2) \/ px=3 /\ (cx=1 \/ cx=2))) Observation mpsc+ringbuf-spinlock Always 558 0 Time mpsc+ringbuf-spinlock 57487.24 Hash=133977dba930d167b4e1b4a6923d5687 Cc: Paul E. McKenney Signed-off-by: Andrii Nakryiko --- .../litmus-tests/mpsc-rb+1p1c+bounded.litmus | 92 +++++++++++ .../litmus-tests/mpsc-rb+1p1c+unbound.litmus | 83 ++++++++++ .../litmus-tests/mpsc-rb+2p1c+bounded.litmus | 152 ++++++++++++++++++ .../litmus-tests/mpsc-rb+2p1c+unbound.litmus | 137 ++++++++++++++++ 4 files changed, 464 insertions(+) create mode 100644 tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus create mode 100644 tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus create mode 100644 tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus create mode 100644 tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus diff --git a/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus new file mode 100644 index 000000000000..cafd17afe11e --- /dev/null +++ b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus @@ -0,0 +1,92 @@ +C mpsc-rb+1p1c+bounded + +(* + * Result: Always + * + * This litmus test validates BPF ring buffer implementation under the + * following assumptions: + * - 1 producer; + * - 1 consumer; + * - ring buffer has capacity for only 1 record. + * + * Expectations: + * - 1 record pushed into ring buffer; + * - 0 or 1 element is consumed. + * - no failures. + *) + +{ + max_len = 1; + len1 = 0; + px = 0; + cx = 0; + dropped = 0; +} + +P0(int *len1, int *cx, int *px) +{ + int *rLenPtr; + int rLen; + int rPx; + int rCx; + int rFail; + + rFail = 0; + rCx = smp_load_acquire(cx); + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } +} + +P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx - rCx >= *max_len) { + atomic_inc(dropped); + spin_unlock(rb_lock); + } else { + if (rPx == 0) + rLenPtr = len1; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); + } +} + +exists ( + 0:rFail=0 /\ 1:rFail=0 + /\ + ( + (dropped=0 /\ px=1 /\ len1=1 /\ (cx=0 \/ cx=1)) + ) +) diff --git a/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus new file mode 100644 index 000000000000..84f660598015 --- /dev/null +++ b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus @@ -0,0 +1,83 @@ +C mpsc-rb+1p1c+unbound + +(* + * Result: Always + * + * This litmus test validates BPF ring buffer implementation under the + * following assumptions: + * - 1 producer; + * - 1 consumer; + * - ring buffer capacity is unbounded. + * + * Expectations: + * - 1 record pushed into ring buffer; + * - 0 or 1 element is consumed. + * - no failures. + *) + +{ + len1 = 0; + px = 0; + cx = 0; +} + +P0(int *len1, int *cx, int *px) +{ + int *rLenPtr; + int rLen; + int rPx; + int rCx; + int rFail; + + rFail = 0; + rCx = smp_load_acquire(cx); + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } +} + +P1(int *len1, spinlock_t *rb_lock, int *px, int *cx) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx == 0) + rLenPtr = len1; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); +} + +exists ( + 0:rFail=0 /\ 1:rFail=0 + /\ px=1 /\ len1=1 + /\ (cx=0 \/ cx=1) +) diff --git a/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus new file mode 100644 index 000000000000..900104c4933b --- /dev/null +++ b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus @@ -0,0 +1,152 @@ +C mpsc-rb+2p1c+bounded + +(* + * Result: Always + * + * This litmus test validates BPF ring buffer implementation under the + * following assumptions: + * - 2 identical producers; + * - 1 consumer; + * - ring buffer has capacity for only 1 record. + * + * Expectations: + * - either 1 or 2 records are pushed into ring buffer; + * - 0, 1, or 2 elements are consumed by consumer; + * - appropriate number of dropped records is recorded to satisfy ring buffer + * size bounds; + * - no failures. + *) + +{ + max_len = 1; + len1 = 0; + px = 0; + cx = 0; + dropped = 0; +} + +P0(int *len1, int *cx, int *px) +{ + int *rLenPtr; + int rLen; + int rPx; + int rCx; + int rFail; + + rFail = 0; + rCx = smp_load_acquire(cx); + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else if (rCx == 1) + rLenPtr = len1; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else if (rCx == 1) + rLenPtr = len1; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } +} + +P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx - rCx >= *max_len) { + atomic_inc(dropped); + spin_unlock(rb_lock); + } else { + if (rPx == 0) + rLenPtr = len1; + else if (rPx == 1) + rLenPtr = len1; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); + } +} + +P2(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx - rCx >= *max_len) { + atomic_inc(dropped); + spin_unlock(rb_lock); + } else { + if (rPx == 0) + rLenPtr = len1; + else if (rPx == 1) + rLenPtr = len1; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); + } +} + +exists ( + 0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 /\ len1=1 + /\ + ( + (dropped = 0 /\ px=2 /\ (cx=1 \/ cx=2)) + \/ + (dropped = 1 /\ px=1 /\ (cx=0 \/ cx=1)) + ) +) diff --git a/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus new file mode 100644 index 000000000000..83372e9eb079 --- /dev/null +++ b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus @@ -0,0 +1,137 @@ +C mpsc-rb+2p1c+unbound + +(* + * Result: Always + * + * This litmus test validates BPF ring buffer implementation under the + * following assumptions: + * - 2 identical producers; + * - 1 consumer; + * - ring buffer capacity is unbounded. + * + * Expectations: + * - 2 records pushed into ring buffer; + * - 0, 1, or 2 elements are consumed. + * - no failures. + *) + +{ + len1 = 0; + len2 = 0; + px = 0; + cx = 0; +} + +P0(int *len1, int *len2, int *cx, int *px) +{ + int *rLenPtr; + int rLen; + int rPx; + int rCx; + int rFail; + + rFail = 0; + rCx = smp_load_acquire(cx); + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else if (rCx == 1) + rLenPtr = len2; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } + + rPx = smp_load_acquire(px); + if (rCx < rPx) { + if (rCx == 0) + rLenPtr = len1; + else if (rCx == 1) + rLenPtr = len2; + else + rFail = 1; + + rLen = smp_load_acquire(rLenPtr); + if (rLen == 0) { + rFail = 1; + } else if (rLen == 1) { + rCx = rCx + 1; + smp_store_release(cx, rCx); + } + } +} + +P1(int *len1, int *len2, spinlock_t *rb_lock, int *px, int *cx) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx == 0) + rLenPtr = len1; + else if (rPx == 1) + rLenPtr = len2; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); +} + +P2(int *len1, int *len2, spinlock_t *rb_lock, int *px, int *cx) +{ + int rPx; + int rCx; + int rFail; + int *rLenPtr; + + rFail = 0; + rCx = smp_load_acquire(cx); + + spin_lock(rb_lock); + + rPx = *px; + if (rPx == 0) + rLenPtr = len1; + else if (rPx == 1) + rLenPtr = len2; + else + rFail = 1; + + *rLenPtr = -1; + smp_wmb(); + smp_store_release(px, rPx + 1); + + spin_unlock(rb_lock); + + smp_store_release(rLenPtr, 1); +} + +exists ( + 0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 + /\ + px=2 /\ len1=1 /\ len2=1 + /\ + (cx=0 \/ cx=1 \/ cx=2) +)