From: Andrea Parri <parri.andrea@gmail.com>
To: Kenneth-Lee-2012@foxmail.com
Cc: Alan Stern <stern@rowland.harvard.edu>,
linux-kernel@vger.kernel.org, paulmck@kernel.org
Subject: Re: Question about PB rule of LKMM
Date: Fri, 8 Mar 2024 22:38:09 +0100 [thread overview]
Message-ID: <ZeuFQdk/zcjkILbC@andrea> (raw)
In-Reply-To: <tencent_3FCF3AA5E98BC9395F98803764A6B2F7CC07@qq.com>
> In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
> it uses the following example to explain the prop relation:
>
> P0()
> {
> int r1;
>
> WRITE_ONCE(x, 1);
> r1 = READ_ONCE(x);
> }
>
> P1()
> {
> WRITE_ONCE(x, 8);
> }
>
> if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
> explained with the operational model. But according to the definition of
> prop,
>
> let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
>
> The link should contain a cumul-fence, which doesn't exist in the
> example.
Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
[Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
(P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
Andrea
next prev parent reply other threads:[~2024-03-08 21:38 UTC|newest]
Thread overview: 23+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-03-01 3:18 Question about PB rule of LKMM Kenneth-Lee-2012
2024-03-05 18:00 ` Andrea Parri
2024-03-06 9:53 ` Kenneth-Lee-2012
2024-03-06 17:36 ` Andrea Parri
2024-03-06 18:29 ` Alan Stern
2024-03-06 19:24 ` Andrea Parri
2024-03-07 0:45 ` Kenneth-Lee-2012
2024-03-07 15:52 ` Andrea Parri
2024-03-07 17:25 ` Alan Stern
2024-03-07 18:18 ` Andrea Parri
2024-03-07 18:30 ` Alan Stern
2024-03-07 19:08 ` Andrea Parri
2024-03-07 19:46 ` Alan Stern
2024-03-07 21:06 ` Andrea Parri
2024-03-08 17:54 ` Alan Stern
2024-03-08 21:29 ` Andrea Parri
2024-03-08 3:10 ` Kenneth-Lee-2012
2024-03-08 21:38 ` Andrea Parri [this message]
2024-03-09 5:43 ` Kenneth-Lee-2012
2024-03-10 2:27 ` Andrea Parri
2024-03-10 2:52 ` Kenneth-Lee-2012
2024-03-11 3:41 ` Kenneth-Lee-2012
[not found] ` <20240311034104.7iffcia4k5rxvgog@kllt01>
2024-03-11 8:20 ` Kenneth-Lee-2012
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=ZeuFQdk/zcjkILbC@andrea \
--to=parri.andrea@gmail.com \
--cc=Kenneth-Lee-2012@foxmail.com \
--cc=linux-kernel@vger.kernel.org \
--cc=paulmck@kernel.org \
--cc=stern@rowland.harvard.edu \
/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 NNTP newsgroup(s).