Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Tue, Apr 03, 2018 at 09:50:19AM -0400, Alan Stern wrote: > On Mon, 2 Apr 2018, Paul E. McKenney wrote: > > > > > I will look at this more later, reaching end of both battery and useful > > > > attention span... > > > > Like the following, perhaps? > > > > Thanx, Paul > > > > > > > > s390 > > > > include "fences.cat" > > include "cos.cat" > > > > (* Fundamental coherence ordering *) > > let com = rf | co | fr > > acyclic po-loc | com as coherence > > > > (* Atomic *) > > empty rmw & (fre;coe) as atom > > > > (* Fences *) > > let mb = [M] ; fencerel(Mb) ; [M] > > > > (* TSO with multicopy atomicity *) > > let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > acyclic mb | po-ghb | fr | rf | co as sc > > Yes, that should work okay (apart from issues related to ordering of > atomic accesses). > > By the way, what does that last "sc" stand for? Surely not Sequential > Consistency! You might consider renaming it to "tso-mca". Good point, fixed. But it is the closest to SC in commercial computing systems, for whatever that is worth. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Tue, Apr 03, 2018 at 09:50:19AM -0400, Alan Stern wrote: > On Mon, 2 Apr 2018, Paul E. McKenney wrote: > > > > > I will look at this more later, reaching end of both battery and useful > > > > attention span... > > > > Like the following, perhaps? > > > > Thanx, Paul > > > > > > > > s390 > > > > include "fences.cat" > > include "cos.cat" > > > > (* Fundamental coherence ordering *) > > let com = rf | co | fr > > acyclic po-loc | com as coherence > > > > (* Atomic *) > > empty rmw & (fre;coe) as atom > > > > (* Fences *) > > let mb = [M] ; fencerel(Mb) ; [M] > > > > (* TSO with multicopy atomicity *) > > let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > acyclic mb | po-ghb | fr | rf | co as sc > > Yes, that should work okay (apart from issues related to ordering of > atomic accesses). > > By the way, what does that last "sc" stand for? Surely not Sequential > Consistency! You might consider renaming it to "tso-mca". Good point, fixed. But it is the closest to SC in commercial computing systems, for whatever that is worth. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Mon, 2 Apr 2018, Paul E. McKenney wrote: > > > I will look at this more later, reaching end of both battery and useful > > > attention span... > > Like the following, perhaps? > > Thanx, Paul > > > > s390 > > include "fences.cat" > include "cos.cat" > > (* Fundamental coherence ordering *) > let com = rf | co | fr > acyclic po-loc | com as coherence > > (* Atomic *) > empty rmw & (fre;coe) as atom > > (* Fences *) > let mb = [M] ; fencerel(Mb) ; [M] > > (* TSO with multicopy atomicity *) > let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > acyclic mb | po-ghb | fr | rf | co as sc Yes, that should work okay (apart from issues related to ordering of atomic accesses). By the way, what does that last "sc" stand for? Surely not Sequential Consistency! You might consider renaming it to "tso-mca". Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Mon, 2 Apr 2018, Paul E. McKenney wrote: > > > I will look at this more later, reaching end of both battery and useful > > > attention span... > > Like the following, perhaps? > > Thanx, Paul > > > > s390 > > include "fences.cat" > include "cos.cat" > > (* Fundamental coherence ordering *) > let com = rf | co | fr > acyclic po-loc | com as coherence > > (* Atomic *) > empty rmw & (fre;coe) as atom > > (* Fences *) > let mb = [M] ; fencerel(Mb) ; [M] > > (* TSO with multicopy atomicity *) > let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > acyclic mb | po-ghb | fr | rf | co as sc Yes, that should work okay (apart from issues related to ordering of atomic accesses). By the way, what does that last "sc" stand for? Surely not Sequential Consistency! You might consider renaming it to "tso-mca". Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Thu, Mar 29, 2018 at 10:40:43AM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > In the meantime, does the cat file look to you like it correctly > > > > models the combination of TSO and multicopy atomicity? Do the > > > > fences really work, or did I just get lucky with my choice of > > > > litmus tests? > > > > > > You got lucky. Try creating an SB litmus test where, instead of an > > > smp_mb() fence between the write and the read, each thread executes > > > some other kind of fence. > > > > Ah, it does indeed get "Never" in that case, which I do not believe > > to e correct. > > > > > The acyclicity condition should have been written more like this: > > > > > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > > > > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > > > > > I don't know what the fence instruction is on s390; change the "mfence" > > > above accordingly. The main difference between this and the > > > corresponding expression in x86tso.cat is that I replaced rfe with rf. > > > > The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on > > how recent of hardware you are running. The latter works everywhere, > > if I recall correctly. But I do not believe that herd knows about either > > instruction yet. > > Herd does not need to understand s390 assembly in order to handle the > things defined in linux.def, such as "smp_mb()". linux.def doesn't > contain any x86 assembly language stuff either (or PPC or ARM). > > > Ah, and I need to lose the "empty rmw & (fre;coe)". > > That appears to be where my spurious ordering was coming from, strange > > though that seems to me. > > No, don't drop it; it was not the source of your spurious ordering. > The extra ordering came from your "(po \ (W * R))" term, which > unintentionally matches fences as well as memory accesses. > > > And your use of "rf" instead of "rfe" makes sense, as that is what makes > > the read-from-write provide ordering, correct? And that should also cover > > the "Uniproc check" that would otherwise be required, right? > > I don't think so... > > > Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... > > Exactly. > > > Which I can fix by unioning po-loc into po-ghb. Or is there some > > better way to do this? > > You could just keep the "uniproc" check. These two approaches accept > the same set of litmus tests. > > Logically, I think of these as two distinct categories of ordering. > po_ghb and tso-mca have to do with the order in which stores reach the > cache, whereas "uniproc" (AKA sequential consistency per variable) has > to do with enforcement of the cache coherence requirements. Clearly > they are related, but they aren't the same thing. > > > > This doesn't account for atomic operations properly; see the "implied" > > > term in x86tso.cat. > > > > I will look at this more later, reaching end of both battery and useful > > attention span... Like the following, perhaps? Thanx, Paul s390 include "fences.cat" include "cos.cat" (* Fundamental coherence ordering *) let com = rf | co | fr acyclic po-loc | com as coherence (* Atomic *) empty rmw & (fre;coe) as atom (* Fences *) let mb = [M] ; fencerel(Mb) ; [M] (* TSO with multicopy atomicity *) let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) acyclic mb | po-ghb | fr | rf | co as sc
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Thu, Mar 29, 2018 at 10:40:43AM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > In the meantime, does the cat file look to you like it correctly > > > > models the combination of TSO and multicopy atomicity? Do the > > > > fences really work, or did I just get lucky with my choice of > > > > litmus tests? > > > > > > You got lucky. Try creating an SB litmus test where, instead of an > > > smp_mb() fence between the write and the read, each thread executes > > > some other kind of fence. > > > > Ah, it does indeed get "Never" in that case, which I do not believe > > to e correct. > > > > > The acyclicity condition should have been written more like this: > > > > > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > > > > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > > > > > I don't know what the fence instruction is on s390; change the "mfence" > > > above accordingly. The main difference between this and the > > > corresponding expression in x86tso.cat is that I replaced rfe with rf. > > > > The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on > > how recent of hardware you are running. The latter works everywhere, > > if I recall correctly. But I do not believe that herd knows about either > > instruction yet. > > Herd does not need to understand s390 assembly in order to handle the > things defined in linux.def, such as "smp_mb()". linux.def doesn't > contain any x86 assembly language stuff either (or PPC or ARM). > > > Ah, and I need to lose the "empty rmw & (fre;coe)". > > That appears to be where my spurious ordering was coming from, strange > > though that seems to me. > > No, don't drop it; it was not the source of your spurious ordering. > The extra ordering came from your "(po \ (W * R))" term, which > unintentionally matches fences as well as memory accesses. > > > And your use of "rf" instead of "rfe" makes sense, as that is what makes > > the read-from-write provide ordering, correct? And that should also cover > > the "Uniproc check" that would otherwise be required, right? > > I don't think so... > > > Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... > > Exactly. > > > Which I can fix by unioning po-loc into po-ghb. Or is there some > > better way to do this? > > You could just keep the "uniproc" check. These two approaches accept > the same set of litmus tests. > > Logically, I think of these as two distinct categories of ordering. > po_ghb and tso-mca have to do with the order in which stores reach the > cache, whereas "uniproc" (AKA sequential consistency per variable) has > to do with enforcement of the cache coherence requirements. Clearly > they are related, but they aren't the same thing. > > > > This doesn't account for atomic operations properly; see the "implied" > > > term in x86tso.cat. > > > > I will look at this more later, reaching end of both battery and useful > > attention span... Like the following, perhaps? Thanx, Paul s390 include "fences.cat" include "cos.cat" (* Fundamental coherence ordering *) let com = rf | co | fr acyclic po-loc | com as coherence (* Atomic *) empty rmw & (fre;coe) as atom (* Fences *) let mb = [M] ; fencerel(Mb) ; [M] (* TSO with multicopy atomicity *) let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) acyclic mb | po-ghb | fr | rf | co as sc
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > In the meantime, does the cat file look to you like it correctly > > > models the combination of TSO and multicopy atomicity? Do the > > > fences really work, or did I just get lucky with my choice of > > > litmus tests? > > > > You got lucky. Try creating an SB litmus test where, instead of an > > smp_mb() fence between the write and the read, each thread executes > > some other kind of fence. > > Ah, it does indeed get "Never" in that case, which I do not believe > to e correct. > > > The acyclicity condition should have been written more like this: > > > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > > > I don't know what the fence instruction is on s390; change the "mfence" > > above accordingly. The main difference between this and the > > corresponding expression in x86tso.cat is that I replaced rfe with rf. > > The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on > how recent of hardware you are running. The latter works everywhere, > if I recall correctly. But I do not believe that herd knows about either > instruction yet. Herd does not need to understand s390 assembly in order to handle the things defined in linux.def, such as "smp_mb()". linux.def doesn't contain any x86 assembly language stuff either (or PPC or ARM). > Ah, and I need to lose the "empty rmw & (fre;coe)". > That appears to be where my spurious ordering was coming from, strange > though that seems to me. No, don't drop it; it was not the source of your spurious ordering. The extra ordering came from your "(po \ (W * R))" term, which unintentionally matches fences as well as memory accesses. > And your use of "rf" instead of "rfe" makes sense, as that is what makes > the read-from-write provide ordering, correct? And that should also cover > the "Uniproc check" that would otherwise be required, right? I don't think so... > Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... Exactly. > Which I can fix by unioning po-loc into po-ghb. Or is there some > better way to do this? You could just keep the "uniproc" check. These two approaches accept the same set of litmus tests. Logically, I think of these as two distinct categories of ordering. po_ghb and tso-mca have to do with the order in which stores reach the cache, whereas "uniproc" (AKA sequential consistency per variable) has to do with enforcement of the cache coherence requirements. Clearly they are related, but they aren't the same thing. > > This doesn't account for atomic operations properly; see the "implied" > > term in x86tso.cat. > > I will look at this more later, reaching end of both battery and useful > attention span... Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > In the meantime, does the cat file look to you like it correctly > > > models the combination of TSO and multicopy atomicity? Do the > > > fences really work, or did I just get lucky with my choice of > > > litmus tests? > > > > You got lucky. Try creating an SB litmus test where, instead of an > > smp_mb() fence between the write and the read, each thread executes > > some other kind of fence. > > Ah, it does indeed get "Never" in that case, which I do not believe > to e correct. > > > The acyclicity condition should have been written more like this: > > > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > > > I don't know what the fence instruction is on s390; change the "mfence" > > above accordingly. The main difference between this and the > > corresponding expression in x86tso.cat is that I replaced rfe with rf. > > The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on > how recent of hardware you are running. The latter works everywhere, > if I recall correctly. But I do not believe that herd knows about either > instruction yet. Herd does not need to understand s390 assembly in order to handle the things defined in linux.def, such as "smp_mb()". linux.def doesn't contain any x86 assembly language stuff either (or PPC or ARM). > Ah, and I need to lose the "empty rmw & (fre;coe)". > That appears to be where my spurious ordering was coming from, strange > though that seems to me. No, don't drop it; it was not the source of your spurious ordering. The extra ordering came from your "(po \ (W * R))" term, which unintentionally matches fences as well as memory accesses. > And your use of "rf" instead of "rfe" makes sense, as that is what makes > the read-from-write provide ordering, correct? And that should also cover > the "Uniproc check" that would otherwise be required, right? I don't think so... > Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... Exactly. > Which I can fix by unioning po-loc into po-ghb. Or is there some > better way to do this? You could just keep the "uniproc" check. These two approaches accept the same set of litmus tests. Logically, I think of these as two distinct categories of ordering. po_ghb and tso-mca have to do with the order in which stores reach the cache, whereas "uniproc" (AKA sequential consistency per variable) has to do with enforcement of the cache coherence requirements. Clearly they are related, but they aren't the same thing. > > This doesn't account for atomic operations properly; see the "implied" > > term in x86tso.cat. > > I will look at this more later, reaching end of both battery and useful > attention span... Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 02:04:07PM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > > > Hello! > > > > > > > > The prototype patch shown below provides files required to allow herd7 > > > > to > > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > > provided by s390. This patch should be viewed with great suspicion. > > > > It does what I expect it to do on SB (with and without barriers), > > > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > > > expectations are quite likely faulty, and my test cases are very few > > > > in number. > > > > > > > > Either way, this is the easy part. The hard part (which I am happy > > > > to leave to others) is making litmus7 and klitmus7 able to do tests > > > > on actual hardware, as well as enabling herd to handle litmus tests > > > > containing BAL. ;-) > > > > > > > > Note that CPU architectures already supported by herd might well need > > > > only a .cfg file that refers to herd's pre-existing support. > > > > > > > > Thoughts? > > > > > > I don't quite see the point of this. You're not suggesting that we > > > have one Linux Kernel Memory Consistency Model for s390 and another > > > one for all the other architectures, are you? > > > > Certainly not for common code! > > > > > If the idea is merely to provide a herd model for s390 then it should > > > go into the DIY repository, not into the LKMM repository. > > > > Makes sense. > > > > In the meantime, does the cat file look to you like it correctly > > models the combination of TSO and multicopy atomicity? Do the > > fences really work, or did I just get lucky with my choice of > > litmus tests? > > You got lucky. Try creating an SB litmus test where, instead of an > smp_mb() fence between the write and the read, each thread executes > some other kind of fence. Ah, it does indeed get "Never" in that case, which I do not believe to e correct. > The acyclicity condition should have been written more like this: > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > I don't know what the fence instruction is on s390; change the "mfence" > above accordingly. The main difference between this and the > corresponding expression in x86tso.cat is that I replaced rfe with rf. The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on how recent of hardware you are running. The latter works everywhere, if I recall correctly. But I do not believe that herd knows about either instruction yet. Ah, and I need to lose the "empty rmw & (fre;coe)". That appears to be where my spurious ordering was coming from, strange though that seems to me. And your use of "rf" instead of "rfe" makes sense, as that is what makes the read-from-write provide ordering, correct? And that should also cover the "Uniproc check" that would otherwise be required, right? Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... Which I can fix by unioning po-loc into po-ghb. Or is there some better way to do this? > This doesn't account for atomic operations properly; see the "implied" > term in x86tso.cat. I will look at this more later, reaching end of both battery and useful attention span... Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 07:51:36PM +0200, Peter Zijlstra wrote: > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > I don't quite see the point of this. You're not suggesting that we > > have one Linux Kernel Memory Consistency Model for s390 and another > > one for all the other architectures, are you? > > > > If the idea is merely to provide a herd model for s390 then it should > > go into the DIY repository, not into the LKMM repository. > > I suspect the use-case was validating s390 arch code which might not > have followed all the regular linux rules because they know its TSO. But > yes, I'm tempted to agree that even arch specific code ought to follow > the regular rules, just to avoid completely messing up the reader. Another use case is testing an s390 .cat file without having to teach herd about s390 assembly. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 02:04:07PM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > > > Hello! > > > > > > > > The prototype patch shown below provides files required to allow herd7 > > > > to > > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > > provided by s390. This patch should be viewed with great suspicion. > > > > It does what I expect it to do on SB (with and without barriers), > > > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > > > expectations are quite likely faulty, and my test cases are very few > > > > in number. > > > > > > > > Either way, this is the easy part. The hard part (which I am happy > > > > to leave to others) is making litmus7 and klitmus7 able to do tests > > > > on actual hardware, as well as enabling herd to handle litmus tests > > > > containing BAL. ;-) > > > > > > > > Note that CPU architectures already supported by herd might well need > > > > only a .cfg file that refers to herd's pre-existing support. > > > > > > > > Thoughts? > > > > > > I don't quite see the point of this. You're not suggesting that we > > > have one Linux Kernel Memory Consistency Model for s390 and another > > > one for all the other architectures, are you? > > > > Certainly not for common code! > > > > > If the idea is merely to provide a herd model for s390 then it should > > > go into the DIY repository, not into the LKMM repository. > > > > Makes sense. > > > > In the meantime, does the cat file look to you like it correctly > > models the combination of TSO and multicopy atomicity? Do the > > fences really work, or did I just get lucky with my choice of > > litmus tests? > > You got lucky. Try creating an SB litmus test where, instead of an > smp_mb() fence between the write and the read, each thread executes > some other kind of fence. Ah, it does indeed get "Never" in that case, which I do not believe to e correct. > The acyclicity condition should have been written more like this: > > let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) > > acyclic mfence | po_ghb | rf | fr | co as tso-mca > > I don't know what the fence instruction is on s390; change the "mfence" > above accordingly. The main difference between this and the > corresponding expression in x86tso.cat is that I replaced rfe with rf. The s390 fence instruction is "bcr 14,0" or "bcr 15,0", depending on how recent of hardware you are running. The latter works everywhere, if I recall correctly. But I do not believe that herd knows about either instruction yet. Ah, and I need to lose the "empty rmw & (fre;coe)". That appears to be where my spurious ordering was coming from, strange though that seems to me. And your use of "rf" instead of "rfe" makes sense, as that is what makes the read-from-write provide ordering, correct? And that should also cover the "Uniproc check" that would otherwise be required, right? Except that I get "Sometimes" on CoWR+poonceonce+Once.litmus... Which I can fix by unioning po-loc into po-ghb. Or is there some better way to do this? > This doesn't account for atomic operations properly; see the "implied" > term in x86tso.cat. I will look at this more later, reaching end of both battery and useful attention span... Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 07:51:36PM +0200, Peter Zijlstra wrote: > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > I don't quite see the point of this. You're not suggesting that we > > have one Linux Kernel Memory Consistency Model for s390 and another > > one for all the other architectures, are you? > > > > If the idea is merely to provide a herd model for s390 then it should > > go into the DIY repository, not into the LKMM repository. > > I suspect the use-case was validating s390 arch code which might not > have followed all the regular linux rules because they know its TSO. But > yes, I'm tempted to agree that even arch specific code ought to follow > the regular rules, just to avoid completely messing up the reader. Another use case is testing an s390 .cat file without having to teach herd about s390 assembly. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > Hello! > > > > > > The prototype patch shown below provides files required to allow herd7 to > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > provided by s390. This patch should be viewed with great suspicion. > > > It does what I expect it to do on SB (with and without barriers), > > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > > expectations are quite likely faulty, and my test cases are very few > > > in number. > > > > > > Either way, this is the easy part. The hard part (which I am happy > > > to leave to others) is making litmus7 and klitmus7 able to do tests > > > on actual hardware, as well as enabling herd to handle litmus tests > > > containing BAL. ;-) > > > > > > Note that CPU architectures already supported by herd might well need > > > only a .cfg file that refers to herd's pre-existing support. > > > > > > Thoughts? > > > > I don't quite see the point of this. You're not suggesting that we > > have one Linux Kernel Memory Consistency Model for s390 and another > > one for all the other architectures, are you? > > Certainly not for common code! > > > If the idea is merely to provide a herd model for s390 then it should > > go into the DIY repository, not into the LKMM repository. > > Makes sense. > > In the meantime, does the cat file look to you like it correctly > models the combination of TSO and multicopy atomicity? Do the > fences really work, or did I just get lucky with my choice of > litmus tests? You got lucky. Try creating an SB litmus test where, instead of an smp_mb() fence between the write and the read, each thread executes some other kind of fence. The acyclicity condition should have been written more like this: let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) acyclic mfence | po_ghb | rf | fr | co as tso-mca I don't know what the fence instruction is on s390; change the "mfence" above accordingly. The main difference between this and the corresponding expression in x86tso.cat is that I replaced rfe with rf. This doesn't account for atomic operations properly; see the "implied" term in x86tso.cat. Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > > > Hello! > > > > > > The prototype patch shown below provides files required to allow herd7 to > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > provided by s390. This patch should be viewed with great suspicion. > > > It does what I expect it to do on SB (with and without barriers), > > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > > expectations are quite likely faulty, and my test cases are very few > > > in number. > > > > > > Either way, this is the easy part. The hard part (which I am happy > > > to leave to others) is making litmus7 and klitmus7 able to do tests > > > on actual hardware, as well as enabling herd to handle litmus tests > > > containing BAL. ;-) > > > > > > Note that CPU architectures already supported by herd might well need > > > only a .cfg file that refers to herd's pre-existing support. > > > > > > Thoughts? > > > > I don't quite see the point of this. You're not suggesting that we > > have one Linux Kernel Memory Consistency Model for s390 and another > > one for all the other architectures, are you? > > Certainly not for common code! > > > If the idea is merely to provide a herd model for s390 then it should > > go into the DIY repository, not into the LKMM repository. > > Makes sense. > > In the meantime, does the cat file look to you like it correctly > models the combination of TSO and multicopy atomicity? Do the > fences really work, or did I just get lucky with my choice of > litmus tests? You got lucky. Try creating an SB litmus test where, instead of an smp_mb() fence between the write and the read, each thread executes some other kind of fence. The acyclicity condition should have been written more like this: let po_ghb = ([R] ; po ; [M]) | ([M] ; po ; [W]) acyclic mfence | po_ghb | rf | fr | co as tso-mca I don't know what the fence instruction is on s390; change the "mfence" above accordingly. The main difference between this and the corresponding expression in x86tso.cat is that I replaced rfe with rf. This doesn't account for atomic operations properly; see the "implied" term in x86tso.cat. Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > I don't quite see the point of this. You're not suggesting that we > have one Linux Kernel Memory Consistency Model for s390 and another > one for all the other architectures, are you? > > If the idea is merely to provide a herd model for s390 then it should > go into the DIY repository, not into the LKMM repository. I suspect the use-case was validating s390 arch code which might not have followed all the regular linux rules because they know its TSO. But yes, I'm tempted to agree that even arch specific code ought to follow the regular rules, just to avoid completely messing up the reader.
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > I don't quite see the point of this. You're not suggesting that we > have one Linux Kernel Memory Consistency Model for s390 and another > one for all the other architectures, are you? > > If the idea is merely to provide a herd model for s390 then it should > go into the DIY repository, not into the LKMM repository. I suspect the use-case was validating s390 arch code which might not have followed all the regular linux rules because they know its TSO. But yes, I'm tempted to agree that even arch specific code ought to follow the regular rules, just to avoid completely messing up the reader.
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 07:20:04AM -0700, Paul E. McKenney wrote: > On Wed, Mar 28, 2018 at 03:48:13PM +0200, Peter Zijlstra wrote: > > On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > > > Hello! > > > > > > The prototype patch shown below provides files required to allow herd7 to > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > provided by s390. > > > > There really isn't anything s390 specific here is there? That is, would > > this not equally work for x86 and sparc, both of which are similarly TSO > > ? > > As I understand it, there is a difference. The difference from TSO > systems such as x86 is that s390 is multicopy atomic as well as TSO. > In contrast, x86 is TSO as well as other-multicopy-atomic. I must defer > to Martin and Christian for details -- this should be interpreted as a > feeble first attempt on my part, not any sort of IBM-approved definition > of s390. ;-) > > > Given that, should this not be called TSO instead of s390 ? > > I agree completely with a single tso.cfg, TSO.cfg, or whatever name, > as opposed to a bunch of identical files for x86, SPARC, ... And to Alan's point, it appears that you can already test x86 TSO ordering on C-language litmus tests as follows: herd7 -conf linux-kernel.cfg -cat x86tso.cat litmus-tests/SB+poonceoncescoh.litmus Might simply be working by accident, but it does currently work. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 07:20:04AM -0700, Paul E. McKenney wrote: > On Wed, Mar 28, 2018 at 03:48:13PM +0200, Peter Zijlstra wrote: > > On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > > > Hello! > > > > > > The prototype patch shown below provides files required to allow herd7 to > > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > > provided by s390. > > > > There really isn't anything s390 specific here is there? That is, would > > this not equally work for x86 and sparc, both of which are similarly TSO > > ? > > As I understand it, there is a difference. The difference from TSO > systems such as x86 is that s390 is multicopy atomic as well as TSO. > In contrast, x86 is TSO as well as other-multicopy-atomic. I must defer > to Martin and Christian for details -- this should be interpreted as a > feeble first attempt on my part, not any sort of IBM-approved definition > of s390. ;-) > > > Given that, should this not be called TSO instead of s390 ? > > I agree completely with a single tso.cfg, TSO.cfg, or whatever name, > as opposed to a bunch of identical files for x86, SPARC, ... And to Alan's point, it appears that you can already test x86 TSO ordering on C-language litmus tests as follows: herd7 -conf linux-kernel.cfg -cat x86tso.cat litmus-tests/SB+poonceoncescoh.litmus Might simply be working by accident, but it does currently work. ;-) Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > Hello! > > > > The prototype patch shown below provides files required to allow herd7 to > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > provided by s390. This patch should be viewed with great suspicion. > > It does what I expect it to do on SB (with and without barriers), > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > expectations are quite likely faulty, and my test cases are very few > > in number. > > > > Either way, this is the easy part. The hard part (which I am happy > > to leave to others) is making litmus7 and klitmus7 able to do tests > > on actual hardware, as well as enabling herd to handle litmus tests > > containing BAL. ;-) > > > > Note that CPU architectures already supported by herd might well need > > only a .cfg file that refers to herd's pre-existing support. > > > > Thoughts? > > I don't quite see the point of this. You're not suggesting that we > have one Linux Kernel Memory Consistency Model for s390 and another > one for all the other architectures, are you? Certainly not for common code! > If the idea is merely to provide a herd model for s390 then it should > go into the DIY repository, not into the LKMM repository. Makes sense. In the meantime, does the cat file look to you like it correctly models the combination of TSO and multicopy atomicity? Do the fences really work, or did I just get lucky with my choice of litmus tests? Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 11:01:25AM -0400, Alan Stern wrote: > On Wed, 28 Mar 2018, Paul E. McKenney wrote: > > > Hello! > > > > The prototype patch shown below provides files required to allow herd7 to > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > provided by s390. This patch should be viewed with great suspicion. > > It does what I expect it to do on SB (with and without barriers), > > IRIW without barriers, and Alan's SB with read-of-write added, but my > > expectations are quite likely faulty, and my test cases are very few > > in number. > > > > Either way, this is the easy part. The hard part (which I am happy > > to leave to others) is making litmus7 and klitmus7 able to do tests > > on actual hardware, as well as enabling herd to handle litmus tests > > containing BAL. ;-) > > > > Note that CPU architectures already supported by herd might well need > > only a .cfg file that refers to herd's pre-existing support. > > > > Thoughts? > > I don't quite see the point of this. You're not suggesting that we > have one Linux Kernel Memory Consistency Model for s390 and another > one for all the other architectures, are you? Certainly not for common code! > If the idea is merely to provide a herd model for s390 then it should > go into the DIY repository, not into the LKMM repository. Makes sense. In the meantime, does the cat file look to you like it correctly models the combination of TSO and multicopy atomicity? Do the fences really work, or did I just get lucky with my choice of litmus tests? Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > Hello! > > The prototype patch shown below provides files required to allow herd7 to > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > provided by s390. This patch should be viewed with great suspicion. > It does what I expect it to do on SB (with and without barriers), > IRIW without barriers, and Alan's SB with read-of-write added, but my > expectations are quite likely faulty, and my test cases are very few > in number. > > Either way, this is the easy part. The hard part (which I am happy > to leave to others) is making litmus7 and klitmus7 able to do tests > on actual hardware, as well as enabling herd to handle litmus tests > containing BAL. ;-) > > Note that CPU architectures already supported by herd might well need > only a .cfg file that refers to herd's pre-existing support. > > Thoughts? I don't quite see the point of this. You're not suggesting that we have one Linux Kernel Memory Consistency Model for s390 and another one for all the other architectures, are you? If the idea is merely to provide a herd model for s390 then it should go into the DIY repository, not into the LKMM repository. Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, 28 Mar 2018, Paul E. McKenney wrote: > Hello! > > The prototype patch shown below provides files required to allow herd7 to > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > provided by s390. This patch should be viewed with great suspicion. > It does what I expect it to do on SB (with and without barriers), > IRIW without barriers, and Alan's SB with read-of-write added, but my > expectations are quite likely faulty, and my test cases are very few > in number. > > Either way, this is the easy part. The hard part (which I am happy > to leave to others) is making litmus7 and klitmus7 able to do tests > on actual hardware, as well as enabling herd to handle litmus tests > containing BAL. ;-) > > Note that CPU architectures already supported by herd might well need > only a .cfg file that refers to herd's pre-existing support. > > Thoughts? I don't quite see the point of this. You're not suggesting that we have one Linux Kernel Memory Consistency Model for s390 and another one for all the other architectures, are you? If the idea is merely to provide a herd model for s390 then it should go into the DIY repository, not into the LKMM repository. Alan
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 03:48:13PM +0200, Peter Zijlstra wrote: > On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > > Hello! > > > > The prototype patch shown below provides files required to allow herd7 to > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > provided by s390. > > There really isn't anything s390 specific here is there? That is, would > this not equally work for x86 and sparc, both of which are similarly TSO > ? As I understand it, there is a difference. The difference from TSO systems such as x86 is that s390 is multicopy atomic as well as TSO. In contrast, x86 is TSO as well as other-multicopy-atomic. I must defer to Martin and Christian for details -- this should be interpreted as a feeble first attempt on my part, not any sort of IBM-approved definition of s390. ;-) > Given that, should this not be called TSO instead of s390 ? I agree completely with a single tso.cfg, TSO.cfg, or whatever name, as opposed to a bunch of identical files for x86, SPARC, ... Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 03:48:13PM +0200, Peter Zijlstra wrote: > On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > > Hello! > > > > The prototype patch shown below provides files required to allow herd7 to > > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > > provided by s390. > > There really isn't anything s390 specific here is there? That is, would > this not equally work for x86 and sparc, both of which are similarly TSO > ? As I understand it, there is a difference. The difference from TSO systems such as x86 is that s390 is multicopy atomic as well as TSO. In contrast, x86 is TSO as well as other-multicopy-atomic. I must defer to Martin and Christian for details -- this should be interpreted as a feeble first attempt on my part, not any sort of IBM-approved definition of s390. ;-) > Given that, should this not be called TSO instead of s390 ? I agree completely with a single tso.cfg, TSO.cfg, or whatever name, as opposed to a bunch of identical files for x86, SPARC, ... Thanx, Paul
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > Hello! > > The prototype patch shown below provides files required to allow herd7 to > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > provided by s390. There really isn't anything s390 specific here is there? That is, would this not equally work for x86 and sparc, both of which are similarly TSO ? Given that, should this not be called TSO instead of s390 ?
Re: [PATCH RFC tools/memory-model] Add s390.{cfg,cat}
On Wed, Mar 28, 2018 at 06:42:32AM -0700, Paul E. McKenney wrote: > Hello! > > The prototype patch shown below provides files required to allow herd7 to > evaluate C-language litmus tests for the multicopy-atomic TSO ordering > provided by s390. There really isn't anything s390 specific here is there? That is, would this not equally work for x86 and sparc, both of which are similarly TSO ? Given that, should this not be called TSO instead of s390 ?
[PATCH RFC tools/memory-model] Add s390.{cfg,cat}
Hello! The prototype patch shown below provides files required to allow herd7 to evaluate C-language litmus tests for the multicopy-atomic TSO ordering provided by s390. This patch should be viewed with great suspicion. It does what I expect it to do on SB (with and without barriers), IRIW without barriers, and Alan's SB with read-of-write added, but my expectations are quite likely faulty, and my test cases are very few in number. Either way, this is the easy part. The hard part (which I am happy to leave to others) is making litmus7 and klitmus7 able to do tests on actual hardware, as well as enabling herd to handle litmus tests containing BAL. ;-) Note that CPU architectures already supported by herd might well need only a .cfg file that refers to herd's pre-existing support. Thoughts? Thanx, Paul commit 2fff0ff161b71215e7f7292b9eff4bc77ba64f29 Author: Paul E. McKenneyDate: Wed Mar 28 06:30:39 2018 -0700 tools/memory-model: Add .cfg and .cat files for s390 This commit adds s390.cat and s390.cfg files to allow users to check litmus tests for s390-specific code. Note that this change only enables herd7 checking of C-language litmus tests. Larger changes are required to enable the litmus7 and klitmus7 tools to check litmus tests on real hardare. Suggested-by: Martin Schwidefsky Suggested-by: Christian Borntraeger Signed-off-by: Paul E. McKenney diff --git a/tools/memory-model/s390.cat b/tools/memory-model/s390.cat new file mode 100644 index ..618e88f50d9a --- /dev/null +++ b/tools/memory-model/s390.cat @@ -0,0 +1,12 @@ +s390 + +include "fences.cat" +include "cos.cat" + +(* Atomic *) +empty rmw & (fre;coe) as atom + +(* TSO with multicopy atomicity *) +acyclic (po \ (W * R)) | po-loc | fr | rf | co as sc + +(* Fences are somehow handled implicitly, at least for SB+mb... *) diff --git a/tools/memory-model/s390.cfg b/tools/memory-model/s390.cfg new file mode 100644 index ..d77e05d2395c --- /dev/null +++ b/tools/memory-model/s390.cfg @@ -0,0 +1,21 @@ +macros linux-kernel.def +bell linux-kernel.bell +model s390.cat +graph columns +squished true +showevents noregs +movelabel true +fontsize 8 +xscale 2.0 +yscale 1.5 +arrowsize 0.8 +showinitrf false +showfinalrf false +showinitwrites false +splines spline +pad 0.1 +edgeattr hb,color,indigo +edgeattr co,color,blue +edgeattr mb,color,darkgreen +edgeattr wmb,color,darkgreen +edgeattr rmb,color,darkgreen
[PATCH RFC tools/memory-model] Add s390.{cfg,cat}
Hello! The prototype patch shown below provides files required to allow herd7 to evaluate C-language litmus tests for the multicopy-atomic TSO ordering provided by s390. This patch should be viewed with great suspicion. It does what I expect it to do on SB (with and without barriers), IRIW without barriers, and Alan's SB with read-of-write added, but my expectations are quite likely faulty, and my test cases are very few in number. Either way, this is the easy part. The hard part (which I am happy to leave to others) is making litmus7 and klitmus7 able to do tests on actual hardware, as well as enabling herd to handle litmus tests containing BAL. ;-) Note that CPU architectures already supported by herd might well need only a .cfg file that refers to herd's pre-existing support. Thoughts? Thanx, Paul commit 2fff0ff161b71215e7f7292b9eff4bc77ba64f29 Author: Paul E. McKenney Date: Wed Mar 28 06:30:39 2018 -0700 tools/memory-model: Add .cfg and .cat files for s390 This commit adds s390.cat and s390.cfg files to allow users to check litmus tests for s390-specific code. Note that this change only enables herd7 checking of C-language litmus tests. Larger changes are required to enable the litmus7 and klitmus7 tools to check litmus tests on real hardare. Suggested-by: Martin Schwidefsky Suggested-by: Christian Borntraeger Signed-off-by: Paul E. McKenney diff --git a/tools/memory-model/s390.cat b/tools/memory-model/s390.cat new file mode 100644 index ..618e88f50d9a --- /dev/null +++ b/tools/memory-model/s390.cat @@ -0,0 +1,12 @@ +s390 + +include "fences.cat" +include "cos.cat" + +(* Atomic *) +empty rmw & (fre;coe) as atom + +(* TSO with multicopy atomicity *) +acyclic (po \ (W * R)) | po-loc | fr | rf | co as sc + +(* Fences are somehow handled implicitly, at least for SB+mb... *) diff --git a/tools/memory-model/s390.cfg b/tools/memory-model/s390.cfg new file mode 100644 index ..d77e05d2395c --- /dev/null +++ b/tools/memory-model/s390.cfg @@ -0,0 +1,21 @@ +macros linux-kernel.def +bell linux-kernel.bell +model s390.cat +graph columns +squished true +showevents noregs +movelabel true +fontsize 8 +xscale 2.0 +yscale 1.5 +arrowsize 0.8 +showinitrf false +showfinalrf false +showinitwrites false +splines spline +pad 0.1 +edgeattr hb,color,indigo +edgeattr co,color,blue +edgeattr mb,color,darkgreen +edgeattr wmb,color,darkgreen +edgeattr rmb,color,darkgreen