Re: [PATCH 1/1] cputime: Make the reported utime+stime correspond to the actual runtime.

[Peter Zijlstra <peterz@infradead.org>]

On Tue, Jul 07, 2015 at 09:59:54AM +0200, Peter Zijlstra wrote:
> > > +	/*
> > > +	 * Make sure stime doesn't go backwards; this preserves monotonicity
> > > +	 * for utime because rtime is monotonic.
> > > +	 *
> > > +	 *  utime_i+1 = rtime_i+1 - stime_i
> > > +	 *            = rtime_i+1 - (rtime_i - stime_i)
> > > +	 *            = (rtime_i+1 - rtime_i) + stime_i
> > > +	 *            >= stime_i
> > > +	 */

Argh, just noticed I messed that up, it should read:

+       /*
+        * Make sure stime doesn't go backwards; this preserves monotonicity
+        * for utime because rtime is monotonic.
+        *
+        *  utime_i+1 = rtime_i+1 - stime_i
+        *            = rtime_i+1 - (rtime_i - utime_i)
+        *            = (rtime_i+1 - rtime_i) + utime_i
+        *            >= utime_i
+        */

I got some [us] confusion. Typing is hard.

So we compute: utime = rtime - stime, which we'll denote as:

	utime_i+1 = rtime_i+1 - stime_i

since: stime_i + utime_i = rtime_i, we can write: stime_i = rtime_i -
utime_i and substitute in the above:

		 = rtime_i+1 - (rtime_i - utime_i)

Rearrange terms:

		= (rtime_i+1 - rtime_i) + utime_i

And since we have: rtime_i+1 >= rtime_i, which we can write like:
rtime_i+1 - rtime_i >= 0, substitution gives:

		>= utime_i

And we've proven that the new utime must be equal or greater than the
previous utime, because rtime is monotonic.