Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Sat, Oct 03, 2020 at 09:22:12AM -0400, Alan Stern wrote:
> To expand on my statement about the LKMM's weakness regarding control 
> constructs, here is a litmus test to illustrate the issue.  You might 
> want to add this to one of the archives.
> 
> Alan
> 
> C crypto-control-data
> (*
>  * LB plus crypto-control-data plus data
>  *
>  * Expected result: allowed
>  *
>  * This is an example of OOTA and we would like it to be forbidden.
>  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
>  * control-dependent on the preceding READ_ONCE.  But the dependencies are
>  * hidden by the form of the conditional control construct, hence the 
>  * name "crypto-control-data".  The memory model doesn't recognize them.
>  *)
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = 1;
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	WRITE_ONCE(*y, r1);
> }
> 
> P1(int *x, int *y)
> {
> 	WRITE_ONCE(*x, READ_ONCE(*y));
> }
> 
> exists (0:r1=1)

Nice simple example!  How about like this?

							Thanx, Paul

------------------------------------------------------------------------

commit c964f404eabe4d8ce294e59dda713d8c19d340cf
Author: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
Date:   Sun Oct 4 16:27:03 2020 -0700

    manual/kernel: Add a litmus test with a hidden dependency
    
    This commit adds a litmus test that has a data dependency that can be
    hidden by control flow.  In this test, both the taken and the not-taken
    branches of an "if" statement must be accounted for in order to properly
    analyze the litmus test.  But herd7 looks only at individual executions
    in isolation, so fails to see the dependency.
    
    Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
    Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>

diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
new file mode 100644
index 0000000..6baecf9
--- /dev/null
+++ b/manual/kernel/crypto-control-data.litmus
@@ -0,0 +1,31 @@
+C crypto-control-data
+(*
+ * LB plus crypto-control-data plus data
+ *
+ * Result: Sometimes
+ *
+ * This is an example of OOTA and we would like it to be forbidden.
+ * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
+ * control-dependent on the preceding READ_ONCE.  But the dependencies are
+ * hidden by the form of the conditional control construct, hence the 
+ * name "crypto-control-data".  The memory model doesn't recognize them.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = 1;
+	if (READ_ONCE(*x) == 0)
+		r1 = 0;
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)