atomic modular increment - is this sound?

This is a function to do an atomic add of 1, mod a
limit, without blocking, for circular buffers. Is
this absolutely free of race conditions? Can anyone prove that?

Cases:

oldval < mod No problem
oldval == mod Returns 0,
*loc incremented to mod+1
*loc has mod subtracted from it
at exit, *loc = 1
oldval > mod Can happen if two threads execute
The first thread will see oldval == mod,
and will reduce *loc by mod. The second
thread will see *loc > mod, and will
not reduce *loc. So for each time oldval
= mod, exactly one subtraction will occur.

John Nagle
Team Overbot

//
// atomic_incmod_value – add to value, modular.
// as atomic operation
//
inline unsigned atomic_incmod_value(volatile unsigned* loc,
unsigned mod)
{ // add 1, return value, atomic operation
if (oldval >= mod) // if overflow
{ if (oldval == mod) // if exactly at overflow
{ atomic_sub(loc,mod); } // must reduce by one cycle
oldval %= mod; // must reduce result
}
return(oldval);
}

John Nagle wrote:

This is a function to do an atomic add of 1, mod a
limit, without blocking, for circular buffers. Is
this absolutely free of race conditions?

I think it is, assuming that “mod” is the same value in
atomic_incmod_value().

Can anyone prove that?

Can’t produce a mathematical proof, but I did excersize
it to my own satisfaction.

Rennie

Rennie Allen wrote:

John Nagle wrote:

This is a function to do an atomic add of 1, mod a
limit, without blocking, for circular buffers. Is
this absolutely free of race conditions?

I think it is, assuming that “mod” is the same value in
atomic_incmod_value().

Yes, that is a constraint. Good point.

Can anyone prove that?

Can’t produce a mathematical proof, but I did excersize
it to my own satisfaction.

Here’s the entire bounded buffer package of which this
is a part.

http://www.overbot.com/public/qnx/

Also in there is “logprintf”, which works like “printf” but
is non-blocking. When the buffer fills, lines
are discarded ("…") appears in the output. Useful for
debug print from real-time programs.

John Nagle
Team Overbot

As of the 9th, your links do not seem to be valid.

Regards,
–Jeff Strickrott

John Nagle wrote:

Rennie Allen wrote:

John Nagle wrote:

This is a function to do an atomic add of 1, mod a
limit, without blocking, for circular buffers. Is
this absolutely free of race conditions?

I think it is, assuming that “mod” is the same value in
atomic_incmod_value().

Yes, that is a constraint. Good point.

Can anyone prove that?

Can’t produce a mathematical proof, but I did excersize
it to my own satisfaction.

Here’s the entire bounded buffer package of which this
is a part.

http://www.overbot.com/public/qnx/

Also in there is “logprintf”, which works like “printf” but
is non-blocking. When the buffer fills, lines
are discarded ("…") appears in the output. Useful for
debug print from real-time programs.

John Nagle
Team Overbot

Sorry, needed to update the site. Thanks.

John Nagle

Jeff Strickrott wrote:

As of the 9th, your links do not seem to be valid.

Regards,
–Jeff Strickrott

John Nagle wrote:

Rennie Allen wrote:

John Nagle wrote:

This is a function to do an atomic add of 1, mod a
limit, without blocking, for circular buffers. Is
this absolutely free of race conditions?

I think it is, assuming that “mod” is the same value in
atomic_incmod_value().

Yes, that is a constraint. Good point.

Can anyone prove that?

Can’t produce a mathematical proof, but I did excersize
it to my own satisfaction.

Here’s the entire bounded buffer package of which this
is a part.

http://www.overbot.com/public/qnx/

Also in there is “logprintf”, which works like “printf” but
is non-blocking. When the buffer fills, lines
are discarded ("…") appears in the output. Useful for
debug print from real-time programs.

John Nagle
Team Overbot