Just to let you know, I've tested your last patch and it solves all my original problems (which is should since the code is functionally equivalent).
/Fredrik On Tue, Jul 7, 2015 at 10:09 AM, Peter Zijlstra <pet...@infradead.org> wrote: > 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. -- /Fredrik -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majord...@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
