From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding; bh=T0MugaJo8WXanWDoVbQME/jXDB+LTggrALf2RbI0vYs=; b=rf/3VFzV+u+rDPSz1GUwMWDjkck9Ax4MGjx9bI7m7/kTomRQKMTqVAxKqZicVQd6uN +cLkqRDRh2GzMEzSj4goECGDYDlKxRugUn5BIcoMBy/y23cteGsxUE1fAFkbuVSo/tka LErVmXKEqolnlt/F52V/1vhcSQptbXQ+XVgaB5bIaOBFbd+Uhcehmm+EYQg6hXdRh/fs mh0Y0MKHOTnSvNA8w1Wup+v+7iE6QUhX24ssyRqeBEOd9jLPEtuMx9MZwVF+VS4rMuWw o960rk66dCBgbHNkC4vb5f0mi62fO9wSTvMX3gp5bgB+o/UGGTKa4uFIMkgH5+/4HuD+ Ilng== Subject: Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests) References: <7e9cc3fb-12af-eb3c-2d81-74486dd9e061@gmail.com> <20201115204244.GM3249@paulmck-ThinkPad-P72> <55d8594a-048d-15f3-b3fc-36ca6594545e@gmail.com> <20201121011410.GT1437@paulmck-ThinkPad-P72> <20201121034714.GV1437@paulmck-ThinkPad-P72> From: Akira Yokosawa Message-ID: <3319ffbf-fc17-b98b-fd68-8ad3c1fa1eac@gmail.com> Date: Sat, 21 Nov 2020 13:14:59 +0900 MIME-Version: 1.0 In-Reply-To: <20201121034714.GV1437@paulmck-ThinkPad-P72> Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 7bit To: paulmck@kernel.org Cc: perfbook@vger.kernel.org, Akira Yokosawa List-ID: On Fri, 20 Nov 2020 19:47:14 -0800, Paul E. McKenney wrote: > On Sat, Nov 21, 2020 at 11:51:11AM +0900, Akira Yokosawa wrote: >> On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote: >>> On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote: >>>> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote: >>>>> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote: >>>>>> Hi Paul, >>>>>> >>>>>> This patch set is what I mentioned the other day in response to >>>>>> your LKMM patch for 5.11. >>>>>> klitmus7 doesn't need most of type info in litmus-test init blocks. >>>>>> >>>>>> While there are some cases where klitmus7 requires type info of variables >>>>>> to be watched (via the "exists", "locations", or "filter" directive), >>>>>> as long as the watched variables are of type "int", extra type info >>>>>> in the init block is not required. >>>>>> >>>>>> Litmus tests under CodeSamples/formal/ should keep compatible with >>>>>> klitmus7 after this patch set is applied. >>>>>> >>>>>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *" >>>>>> under CodeSamples/formal/litmus/. >>>>>> >>>>>> Patch 2/2 further reduce line counts of litmus tests by using "{}" >>>>>> as empty init blocks. >>>>>> It also adds/removes empty lines for those code snippets to have >>>>>> consistent looks. >>>>>> >>>>>> Similar changes to patch 1/2 can be made in the RCU litmus tests >>>>>> presented in Section 12.3.2. They are not touched in this patch set. >>>>>> >>>>>> May be in a follow-up patch. >>>>> >>>>> Queued and pushed, thank you very much! >>>>> >>>>>> Thanks, Akira >>>>>> >>>>>> *NOTE*: >>>>>> >>>>>> There are cases where litmus tests for herd7 can not be >>>>>> made compatible with (current) klitmus7, though. >>>>>> >>>>>> One such example is when a variable of a type other than the "int" >>>>>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter" >>>>>> directive. >>>>>> Current klitmus7 has no idea of the way to obtain the value of such a >>>>>> variable. >>>>> >>>>> Good to know! Do we have litmus tests that have problems with this? >>>> >>>> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus >>> >>> So there is not currently such a litmus test in perfbook, but one could >>> easily be created, correct? >> >> You are right! >> >> Thanks, Akira >> >> PS. >> >> I'm preparing a patch series to add an index framework in perfbook. >> My plan is to add a specific make target for the time being to have such >> index pages printed. >> As you should know, the hard part is to embed a *lot* of index annotations >> in .tex source files. > > Quite right, it is a big job! > >> I'm thinking of splitting indexes into a general one and API index. >> By API, I mean functions such as smp_mb(), READ_ONCE(), etc. >> >> API index can have kernel API, perfbook specific API, C11 API, and GCC API. > > The upside is that the individual indexes are smaller and perhaps > more manageable. The downside is that a reader who has no idea > what the function call is might have to look it up in four (or maybe > even five) indexes. Especially if the API is a historic API that > is no longer used. > > I have no idea what the right answer is. One approach would be to > have all of the APIs appear both in their respective categories and > in the general index. Not sure that this would be any better, though. My idea is to merge all the APIs into a single API Index. Category of each API can be shown there like: __atomic_load() (GCC), ACCESS_ONCE() (kernel, historic), atomic_inc() (kernel), atomic_load() (C11), fork() (POSIX), smp_mb() (kernel), smp_read_barrier_depends() (kernel, historic), Give or take the appearance of annotations. For example we can use "G" for "GCC", "C" for "C11", "k" for "kernel", "k,h" for "kernel, historic", etc. > >> As for words/terms, if you can provide me a wish list you'd like to see in >> the general index, I'm willing to add such annotations. >> My starting point of the general index is the Glossary. > > The glossary is a good starting point. People mentioned in the text is > another. Not sure whether or not those quoted in the epigraphs should > be included or not. Ah, I missed people's names. > Names of algorithms should be included, also names > of data structures and of famous problems (for example, the Dining > Philosopher's problem, mazes, and so on). > > I am sure that I am missing quite a few categories, but at least a > start! ;-) Let me see how it can be done. I'll submit a [NOT PULL] request when it is ready as PoC. Thanks, Akira > > Thanx, Paul > >> Thoughts? >> >>> >>> Or am I still confused? ;-) >>> >>> Thanx, Paul >>> >>>> --- >>>> C Lock1-for-herd7 >>>> >>>> (* >>>> * Example test incompatible with klitmus7 >>>> * >>>> * klitmus7 cannot access spinlock_t variable. >>>> *) >>>> >>>> {} >>>> >>>> P0(int *x, spinlock_t *sp) >>>> { >>>> spin_lock(sp); >>>> WRITE_ONCE(*x, 1); >>>> WRITE_ONCE(*x, 0); >>>> spin_unlock(sp); >>>> } >>>> >>>> P1(int *x, spinlock_t *sp) >>>> { >>>> int r1; >>>> >>>> spin_lock(sp); >>>> r1 = READ_ONCE(*x); >>>> spin_unlock(sp); >>>> } >>>> >>>> locations [sp] (* incompatible with klitmus7 *) >>>> exists (1:r1=1) >>>> --- >>>> >>>> klitmus7 can't convert this to a kernel module: >>>> >>>> --- >>>> $ klitmus7 -o temp C-Lock1-for-herd7.litmus >>>> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t >>>> --- >>>> >>>> Actually, herd7/LKMM does complain of this one: >>>> >>>> --- >>>> Test Lock1-for-herd7 Allowed >>>> States 1 >>>> 1:r1=0; sp=0; >>>> No >>>> Witnesses >>>> Positive: 0 Negative: 2 >>>> Flag lock-final <--- >>>> Condition exists (1:r1=1) >>>> Observation Lock1-for-herd7 Never 0 2 >>>> Time Lock1-for-herd7 0.01 >>>> Hash=5d10e6c355cec0c36f354abf175adc54 >>>> --- >>>> >>>> Comment at line 57 of lock.cat says: >>>> >>>> --- >>>> (* The final value of a spinlock should not be tested *) >>>> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final >>>> --- >>>> >>>> Thanks, Akira >>>> >> >> [...]