Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Paul E. McKenney]

On Sat, Apr 22, 2017 at 10:17:11AM -0700, priyalee.kushwaha@intel.com wrote:
> From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> 
> Most OS distribution have awk in /usr/bin not in /bin
> Without this patch, kernel-devsrc fails to build as
> runtime dependency for srcu-cbmc script /bin/awk is
> not found.

Adding Lance on CC.

							Thanx, Paul

> Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> ---
>  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> index 8ff8904..c9e8bc5 100755
> --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> @@ -1,4 +1,4 @@
> -#!/bin/awk -f
> +#!/usr/bin/awk -f
> 
>  # Modify SRCU for formal verification. The first argument should be srcu.h and
>  # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
> -- 
> 2.10.0
> 

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Josh Triplett]

On Sat, Apr 22, 2017 at 10:17:11AM -0700, priyalee.kushwaha@intel.com wrote:
> From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> 
> Most OS distribution have awk in /usr/bin not in /bin
> Without this patch, kernel-devsrc fails to build as
> runtime dependency for srcu-cbmc script /bin/awk is
> not found.
> 
> Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>

For anyone that has it in /bin/awk, does it have a compatibility symlink
from /usr/bin/awk (or vice versa), or not?  If not, then this would
break the build for those folks.

We could just drop the shebang and the executable bit, and run "awk -f
modify_srcu.awk" from whatever script invokes this.

>  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> index 8ff8904..c9e8bc5 100755
> --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> @@ -1,4 +1,4 @@
> -#!/bin/awk -f
> +#!/usr/bin/awk -f
>  
>  # Modify SRCU for formal verification. The first argument should be srcu.h and
>  # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
> -- 
> 2.10.0
> 

RE: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Kushwaha, Priyalee]

Tested 9 distros centos, Debian, Fedora, Gentoo, Opensuse, slackware, Ubuntu, poky showed awk at /usr/bin/awk. 

Here is another similar patch which has been approved https://patchwork.kernel.org/patch/9650581/

centos-7:
lrwxrwxrwx 1 root root 4 Mar 15 19:58 /bin/awk -> gawk lrwxrwxrwx 1 root root 4 Mar 15 19:58 /usr/bin/awk -> gawk

Debian-8:
ls: cannot access /bin/awk: No such file or directory lrwxrwxrwx 1 root root 21 Mar 20 23:26 /usr/bin/awk -> /etc/alternatives/awk

Fedora:
lrwxrwxrwx. 1 root root 4 Sep 12  2016 /bin/awk -> gawk lrwxrwxrwx. 1 root root 4 Sep 12  2016 /usr/bin/awk -> gawk

Gentoo:
lrwxrwxrwx 1 root root 15 Jan  1 13:57 /bin/awk -> ../usr/bin/gawk lrwxrwxrwx 1 root root  4 Jan  1 13:57 /usr/bin/awk -> gawk

Opensuse:
lrwxrwxrwx 1 root root 21 Mar 20 11:19 /bin/awk -> /etc/alternatives/awk lrwxrwxrwx 1 root root 29 Mar 20 11:19 /usr/bin/awk -> /etc/alternatives/usr-bin-awk

Slackware:
lrwxrwxrwx 1 root root  4 Mar 10 15:37 /bin/awk -> gawk lrwxrwxrwx 1 root root 13 Mar 10 15:37 /usr/bin/awk -> ../../bin/awk

Ubuntu:
ls: cannot access '/bin/awk': No such file or directory lrwxrwxrwx 1 root root 21 Dec  6  2015 /usr/bin/awk -> /etc/alternatives/awk

Poky:
ls: /bin/awk: No such file or directory
lrwxrwxrwx    1 root     root            19 Apr 20 22:59 /usr/bin/awk

-----Original Message-----
From: Josh Triplett [mailto:josh@joshtriplett.org] 
Sent: Friday, April 21, 2017 11:48 AM
To: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
Cc: paulmck@linux.vnet.ibm.com; shuah@kernel.org; linux-kernel@vger.kernel.org; linux-kselftest@vger.kernel.org
Subject: Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

On Sat, Apr 22, 2017 at 10:17:11AM -0700, priyalee.kushwaha@intel.com wrote:
> From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> 
> Most OS distribution have awk in /usr/bin not in /bin Without this 
> patch, kernel-devsrc fails to build as runtime dependency for 
> srcu-cbmc script /bin/awk is not found.
> 
> Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>

For anyone that has it in /bin/awk, does it have a compatibility symlink from /usr/bin/awk (or vice versa), or not?  If not, then this would break the build for those folks.

We could just drop the shebang and the executable bit, and run "awk -f modify_srcu.awk" from whatever script invokes this.

>  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 
> 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git 
> a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk 
> b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> index 8ff8904..c9e8bc5 100755
> --- 
> a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.
> +++ awk
> @@ -1,4 +1,4 @@
> -#!/bin/awk -f
> +#!/usr/bin/awk -f
>  
>  # Modify SRCU for formal verification. The first argument should be 
> srcu.h and  # the second should be srcu.c. Outputs modified srcu.h and 
> srcu.c into the
> --
> 2.10.0
> 

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Josh Triplett]

On Fri, Apr 21, 2017 at 09:52:10PM +0000, Kushwaha, Priyalee wrote:
> Tested 9 distros centos, Debian, Fedora, Gentoo, Opensuse, slackware, Ubuntu, poky showed awk at /usr/bin/awk. 
> 
> Here is another similar patch which has been approved https://patchwork.kernel.org/patch/9650581/
> 
> centos-7:
> lrwxrwxrwx 1 root root 4 Mar 15 19:58 /bin/awk -> gawk lrwxrwxrwx 1 root root 4 Mar 15 19:58 /usr/bin/awk -> gawk
> 
> Debian-8:
> ls: cannot access /bin/awk: No such file or directory lrwxrwxrwx 1 root root 21 Mar 20 23:26 /usr/bin/awk -> /etc/alternatives/awk
> 
> Fedora:
> lrwxrwxrwx. 1 root root 4 Sep 12  2016 /bin/awk -> gawk lrwxrwxrwx. 1 root root 4 Sep 12  2016 /usr/bin/awk -> gawk
> 
> Gentoo:
> lrwxrwxrwx 1 root root 15 Jan  1 13:57 /bin/awk -> ../usr/bin/gawk lrwxrwxrwx 1 root root  4 Jan  1 13:57 /usr/bin/awk -> gawk
> 
> Opensuse:
> lrwxrwxrwx 1 root root 21 Mar 20 11:19 /bin/awk -> /etc/alternatives/awk lrwxrwxrwx 1 root root 29 Mar 20 11:19 /usr/bin/awk -> /etc/alternatives/usr-bin-awk
> 
> Slackware:
> lrwxrwxrwx 1 root root  4 Mar 10 15:37 /bin/awk -> gawk lrwxrwxrwx 1 root root 13 Mar 10 15:37 /usr/bin/awk -> ../../bin/awk
> 
> Ubuntu:
> ls: cannot access '/bin/awk': No such file or directory lrwxrwxrwx 1 root root 21 Dec  6  2015 /usr/bin/awk -> /etc/alternatives/awk
> 
> Poky:
> ls: /bin/awk: No such file or directory
> lrwxrwxrwx    1 root     root            19 Apr 20 22:59 /usr/bin/awk

This seems fairly conclusive.  Based on this, switching over to
/usr/bin/awk seems fine.

[PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[priyalee.kushwaha]

From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>

Most OS distribution have awk in /usr/bin not in /bin
Without this patch, kernel-devsrc fails to build as
runtime dependency for srcu-cbmc script /bin/awk is
not found.

Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
---
 tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
index 8ff8904..c9e8bc5 100755
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
@@ -1,4 +1,4 @@
-#!/bin/awk -f
+#!/usr/bin/awk -f
 
 # Modify SRCU for formal verification. The first argument should be srcu.h and
 # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
-- 
2.10.0

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Paul E. McKenney]

On Fri, Apr 21, 2017 at 03:05:49PM -0700, Josh Triplett wrote:
> On Fri, Apr 21, 2017 at 09:52:10PM +0000, Kushwaha, Priyalee wrote:
> > Tested 9 distros centos, Debian, Fedora, Gentoo, Opensuse, slackware, Ubuntu, poky showed awk at /usr/bin/awk. 
> > 
> > Here is another similar patch which has been approved https://patchwork.kernel.org/patch/9650581/
> > 
> > centos-7:
> > lrwxrwxrwx 1 root root 4 Mar 15 19:58 /bin/awk -> gawk lrwxrwxrwx 1 root root 4 Mar 15 19:58 /usr/bin/awk -> gawk
> > 
> > Debian-8:
> > ls: cannot access /bin/awk: No such file or directory lrwxrwxrwx 1 root root 21 Mar 20 23:26 /usr/bin/awk -> /etc/alternatives/awk
> > 
> > Fedora:
> > lrwxrwxrwx. 1 root root 4 Sep 12  2016 /bin/awk -> gawk lrwxrwxrwx. 1 root root 4 Sep 12  2016 /usr/bin/awk -> gawk
> > 
> > Gentoo:
> > lrwxrwxrwx 1 root root 15 Jan  1 13:57 /bin/awk -> ../usr/bin/gawk lrwxrwxrwx 1 root root  4 Jan  1 13:57 /usr/bin/awk -> gawk
> > 
> > Opensuse:
> > lrwxrwxrwx 1 root root 21 Mar 20 11:19 /bin/awk -> /etc/alternatives/awk lrwxrwxrwx 1 root root 29 Mar 20 11:19 /usr/bin/awk -> /etc/alternatives/usr-bin-awk
> > 
> > Slackware:
> > lrwxrwxrwx 1 root root  4 Mar 10 15:37 /bin/awk -> gawk lrwxrwxrwx 1 root root 13 Mar 10 15:37 /usr/bin/awk -> ../../bin/awk
> > 
> > Ubuntu:
> > ls: cannot access '/bin/awk': No such file or directory lrwxrwxrwx 1 root root 21 Dec  6  2015 /usr/bin/awk -> /etc/alternatives/awk
> > 
> > Poky:
> > ls: /bin/awk: No such file or directory
> > lrwxrwxrwx    1 root     root            19 Apr 20 22:59 /usr/bin/awk
> 
> This seems fairly conclusive.  Based on this, switching over to
> /usr/bin/awk seems fine.

Thank you both!  Josh, may I have your Acked-by?

							Thanx, Paul

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Lance Roy]

This is fine with me. I didn't notice that /bin/awk was just a symlink on the
distro I was using when I wrote the script.

Thanks,
Lance

On Fri, 21 Apr 2017 10:50:42 -0700
"Paul E. McKenney" <paulmck@linux.vnet.ibm.com> wrote:

> On Sat, Apr 22, 2017 at 10:17:11AM -0700, priyalee.kushwaha@intel.com wrote:
> > From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> >
> > Most OS distribution have awk in /usr/bin not in /bin
> > Without this patch, kernel-devsrc fails to build as
> > runtime dependency for srcu-cbmc script /bin/awk is
> > not found.
>
> Adding Lance on CC.
>
> 							Thanx, Paul
>
> > Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> > ---
> >  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> >
> > diff --git
> > a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> > b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk index
> > 8ff8904..c9e8bc5 100755 ---
> > a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk +++
> > b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk @@
> > -1,4 +1,4 @@ -#!/bin/awk -f +#!/usr/bin/awk -f
> >
> >  # Modify SRCU for formal verification. The first argument should be srcu.h
> > and # the second should be srcu.c. Outputs modified srcu.h and srcu.c into
> > the --
> > 2.10.0
> >
>

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Paul E. McKenney]

On Sun, Apr 23, 2017 at 08:24:11PM -0700, Lance Roy wrote:
> This is fine with me. I didn't notice that /bin/awk was just a symlink on the
> distro I was using when I wrote the script.

Very good!  May I please have your Acked-by?

							Thanx, Paul

> Thanks,
> Lance
> 
> On Fri, 21 Apr 2017 10:50:42 -0700
> "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> wrote:
> 
> > On Sat, Apr 22, 2017 at 10:17:11AM -0700, priyalee.kushwaha@intel.com wrote:
> > > From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> > >
> > > Most OS distribution have awk in /usr/bin not in /bin
> > > Without this patch, kernel-devsrc fails to build as
> > > runtime dependency for srcu-cbmc script /bin/awk is
> > > not found.
> >
> > Adding Lance on CC.
> >
> > 							Thanx, Paul
> >
> > > Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> > > ---
> > >  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
> > >  1 file changed, 1 insertion(+), 1 deletion(-)
> > >
> > > diff --git
> > > a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> > > b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk index
> > > 8ff8904..c9e8bc5 100755 ---
> > > a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk +++
> > > b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk @@
> > > -1,4 +1,4 @@ -#!/bin/awk -f +#!/usr/bin/awk -f
> > >
> > >  # Modify SRCU for formal verification. The first argument should be srcu.h
> > > and # the second should be srcu.c. Outputs modified srcu.h and srcu.c into
> > > the --
> > > 2.10.0
> > >
> >
> 

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Lance Roy]

Acked-by: Lance Roy <ldr709@gmail.com>

On Sat, 22 Apr 2017 10:17:11 -0700
priyalee.kushwaha@intel.com wrote:

> From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
>
> Most OS distribution have awk in /usr/bin not in /bin
> Without this patch, kernel-devsrc fails to build as
> runtime dependency for srcu-cbmc script /bin/awk is
> not found.
>
> Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> ---
>  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
>
> diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> index 8ff8904..c9e8bc5 100755
> --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> @@ -1,4 +1,4 @@
> -#!/bin/awk -f
> +#!/usr/bin/awk -f
>
>  # Modify SRCU for formal verification. The first argument should be srcu.h and
>  # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Josh Triplett]

On April 23, 2017 7:44:48 PM PDT, "Paul E. McKenney" <paulmck@linux.vnet.ibm.com> wrote:
>On Fri, Apr 21, 2017 at 03:05:49PM -0700, Josh Triplett wrote:
>> On Fri, Apr 21, 2017 at 09:52:10PM +0000, Kushwaha, Priyalee wrote:
>> > Tested 9 distros centos, Debian, Fedora, Gentoo, Opensuse,
>slackware, Ubuntu, poky showed awk at /usr/bin/awk. 
>> > 
>> > Here is another similar patch which has been approved
>https://patchwork.kernel.org/patch/9650581/
>> > 
>> > centos-7:
>> > lrwxrwxrwx 1 root root 4 Mar 15 19:58 /bin/awk -> gawk lrwxrwxrwx 1
>root root 4 Mar 15 19:58 /usr/bin/awk -> gawk
>> > 
>> > Debian-8:
>> > ls: cannot access /bin/awk: No such file or directory lrwxrwxrwx 1
>root root 21 Mar 20 23:26 /usr/bin/awk -> /etc/alternatives/awk
>> > 
>> > Fedora:
>> > lrwxrwxrwx. 1 root root 4 Sep 12  2016 /bin/awk -> gawk lrwxrwxrwx.
>1 root root 4 Sep 12  2016 /usr/bin/awk -> gawk
>> > 
>> > Gentoo:
>> > lrwxrwxrwx 1 root root 15 Jan  1 13:57 /bin/awk -> ../usr/bin/gawk
>lrwxrwxrwx 1 root root  4 Jan  1 13:57 /usr/bin/awk -> gawk
>> > 
>> > Opensuse:
>> > lrwxrwxrwx 1 root root 21 Mar 20 11:19 /bin/awk ->
>/etc/alternatives/awk lrwxrwxrwx 1 root root 29 Mar 20 11:19
>/usr/bin/awk -> /etc/alternatives/usr-bin-awk
>> > 
>> > Slackware:
>> > lrwxrwxrwx 1 root root  4 Mar 10 15:37 /bin/awk -> gawk lrwxrwxrwx
>1 root root 13 Mar 10 15:37 /usr/bin/awk -> ../../bin/awk
>> > 
>> > Ubuntu:
>> > ls: cannot access '/bin/awk': No such file or directory lrwxrwxrwx
>1 root root 21 Dec  6  2015 /usr/bin/awk -> /etc/alternatives/awk
>> > 
>> > Poky:
>> > ls: /bin/awk: No such file or directory
>> > lrwxrwxrwx    1 root     root            19 Apr 20 22:59
>/usr/bin/awk
>> 
>> This seems fairly conclusive.  Based on this, switching over to
>> /usr/bin/awk seems fine.
>
>Thank you both!  Josh, may I have your Acked-by?

Reviewed-by: Josh Triplett <josh@joshtriplett.org>

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Shuah Khan]

On 04/22/2017 11:17 AM, priyalee.kushwaha@intel.com wrote:
> From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> 
> Most OS distribution have awk in /usr/bin not in /bin
> Without this patch, kernel-devsrc fails to build as
> runtime dependency for srcu-cbmc script /bin/awk is
> not found.
> 
> Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> ---
>  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> index 8ff8904..c9e8bc5 100755
> --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> @@ -1,4 +1,4 @@
> -#!/bin/awk -f
> +#!/usr/bin/awk -f
>  
>  # Modify SRCU for formal verification. The first argument should be srcu.h and
>  # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
> 

Hi Paul,

If this change looks good, please Ack it so I can take it through kselftest
tree. If you would like to take this through rcu, that is fine as well.

thanks,
-- Shuah

Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Paul E. McKenney]

On Mon, Apr 24, 2017 at 08:02:10AM -0600, Shuah Khan wrote:
> On 04/22/2017 11:17 AM, priyalee.kushwaha@intel.com wrote:
> > From: Priyalee Kushwaha <priyalee.kushwaha@intel.com>
> > 
> > Most OS distribution have awk in /usr/bin not in /bin
> > Without this patch, kernel-devsrc fails to build as
> > runtime dependency for srcu-cbmc script /bin/awk is
> > not found.
> > 
> > Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
> > ---
> >  tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> > 
> > diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> > index 8ff8904..c9e8bc5 100755
> > --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> > +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
> > @@ -1,4 +1,4 @@
> > -#!/bin/awk -f
> > +#!/usr/bin/awk -f
> >  
> >  # Modify SRCU for formal verification. The first argument should be srcu.h and
> >  # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
> > 
> 
> Hi Paul,
> 
> If this change looks good, please Ack it so I can take it through kselftest
> tree. If you would like to take this through rcu, that is fine as well.

Hello, Shuah,

I have queued it with Lance's ack and Josh's review.

Just for full disclosure, my recent SRCU work has broken srcu-cbmc,
and a bit more breakage is on its way.  :-(

That said, I would welcome patches to fix it -- mostly adjustments in
pathnames, structure names, and which fields get removed.  Adjusting it
to work correctly with Classic SRCU would probably be a bit easier than
adapting it to either Tree SRCU or Tiny SRCU.

							Thanx, Paul