~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

TOMOYO Linux Cross Reference
Linux/Documentation/litmus-tests/locking/DCL-fixed.litmus

Version: ~ [ linux-6.12-rc7 ] ~ [ linux-6.11.7 ] ~ [ linux-6.10.14 ] ~ [ linux-6.9.12 ] ~ [ linux-6.8.12 ] ~ [ linux-6.7.12 ] ~ [ linux-6.6.60 ] ~ [ linux-6.5.13 ] ~ [ linux-6.4.16 ] ~ [ linux-6.3.13 ] ~ [ linux-6.2.16 ] ~ [ linux-6.1.116 ] ~ [ linux-6.0.19 ] ~ [ linux-5.19.17 ] ~ [ linux-5.18.19 ] ~ [ linux-5.17.15 ] ~ [ linux-5.16.20 ] ~ [ linux-5.15.171 ] ~ [ linux-5.14.21 ] ~ [ linux-5.13.19 ] ~ [ linux-5.12.19 ] ~ [ linux-5.11.22 ] ~ [ linux-5.10.229 ] ~ [ linux-5.9.16 ] ~ [ linux-5.8.18 ] ~ [ linux-5.7.19 ] ~ [ linux-5.6.19 ] ~ [ linux-5.5.19 ] ~ [ linux-5.4.285 ] ~ [ linux-5.3.18 ] ~ [ linux-5.2.21 ] ~ [ linux-5.1.21 ] ~ [ linux-5.0.21 ] ~ [ linux-4.20.17 ] ~ [ linux-4.19.323 ] ~ [ linux-4.18.20 ] ~ [ linux-4.17.19 ] ~ [ linux-4.16.18 ] ~ [ linux-4.15.18 ] ~ [ linux-4.14.336 ] ~ [ linux-4.13.16 ] ~ [ linux-4.12.14 ] ~ [ linux-4.11.12 ] ~ [ linux-4.10.17 ] ~ [ linux-4.9.337 ] ~ [ linux-4.4.302 ] ~ [ linux-3.10.108 ] ~ [ linux-2.6.32.71 ] ~ [ linux-2.6.0 ] ~ [ linux-2.4.37.11 ] ~ [ unix-v6-master ] ~ [ ccs-tools-1.8.12 ] ~ [ policy-sample ] ~
Architecture: ~ [ i386 ] ~ [ alpha ] ~ [ m68k ] ~ [ mips ] ~ [ ppc ] ~ [ sparc ] ~ [ sparc64 ] ~

  1 C DCL-fixed
  2 
  3 (*
  4  * Result: Never
  5  *
  6  * This litmus test demonstrates that double-checked locking can be
  7  * reliable given proper use of smp_load_acquire() and smp_store_release()
  8  * in addition to the locking.
  9  *)
 10 
 11 {
 12         int flag;
 13         int data;
 14 }
 15 
 16 P0(int *flag, int *data, spinlock_t *lck)
 17 {
 18         int r0;
 19         int r1;
 20         int r2;
 21 
 22         r0 = smp_load_acquire(flag);
 23         if (r0 == 0) {
 24                 spin_lock(lck);
 25                 r1 = READ_ONCE(*flag);
 26                 if (r1 == 0) {
 27                         WRITE_ONCE(*data, 1);
 28                         smp_store_release(flag, 1);
 29                 }
 30                 spin_unlock(lck);
 31         }
 32         r2 = READ_ONCE(*data);
 33 }
 34 
 35 P1(int *flag, int *data, spinlock_t *lck)
 36 {
 37         int r0;
 38         int r1;
 39         int r2;
 40 
 41         r0 = smp_load_acquire(flag);
 42         if (r0 == 0) {
 43                 spin_lock(lck);
 44                 r1 = READ_ONCE(*flag);
 45                 if (r1 == 0) {
 46                         WRITE_ONCE(*data, 1);
 47                         smp_store_release(flag, 1);
 48                 }
 49                 spin_unlock(lck);
 50         }
 51         r2 = READ_ONCE(*data);
 52 }
 53 
 54 locations [flag;data;0:r0;0:r1;1:r0;1:r1]
 55 exists (0:r2=0 \/ 1:r2=0)

~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

kernel.org | git.kernel.org | LWN.net | Project Home | SVN repository | Mail admin

Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.

sflogo.php