- Mathematics in Action: What jobs have been running too long
- : Purpose
- : Background
- : Examples
- : Quality Requirement
- : Note
- : Formal Analysis
- : C and C++ Code
- : Actual Implementation
- : Testing
- : Conclusion
- Proof of 5
- Proof of 11
- Proof of 15
- Proof of 18
- Notes

- s::int=the start time,
- S::0..23=the start time on the 24 hour clock.
- t::int=the time now,
- T::0..23=the time on the 24 hour clock.
- g::0..23=the grace period in hours.
Given

- D::int=T-S, we want to determine if
- d::int=t-s is
- d > g or d<=g.
We will use the C/C++ notation for remainder or modulus:

- For int i,j>0, i%j::=i - j*(i/j).
We can show that
- (above)|- (r0): For i,j>0, i=i%j+j*(i/j).
- (above)|- (r1): For i,j>0, for some k(i=k*j+i%j)).
- (the|-symbol is used to indicate that a formaula has been asserted to be
true)
We have been told:

- |- (1): T = t % 24
- |- (2): S = s % 24
- |- (3): 0 <= t-s and t-s < 24.
So we deduce:

- (1, 2)|- (4): (T-S)%24 = (t-s)%24.
- (4, r1)|- (5): for some k, d = D + 24*k
- (1, 2)|- (6): 0 <= T and S < 24,
- (6, 3)|- (7): d in { D, D+24, D+48, ...} and 0..23
- = { D, D+24 }.
Now

- (above)|- (D0): D<0 or D=0 or D>0.
- (7, 5)|- (11): if D=0 then d<g.
- (6, 7)|- (15): if D<0 then ( d<g iff D+24<g ).
- (7)|- (18): if D>0 then (d<g iff D<g).
- (D0, 11, 15, 18)|- (20): if D<0 then (d<g iff D+24<g) else (d<g iff D<g).
## C and C++ Code

We would therefore use the following functionint (int T, int S, int g)

{

if (T-S < 0)

return T-S+24 < g;

else

return T-S < g;

}

## Actual Implementation

The "ftp.hangman" program is a shell script:: Hang up day old FTP sessions. Uses BSD -u option, RTFM

tmp=/tmp/ftp.hang.$$

ps -axu >$tmp

grep "^ftp" <$tmp |

awk '$9!~/:/{print $2}' |

while read pid; do kill -9 $pid; done

rm $tmp

This works because the set of running jobs is listed in

*tmp*by the ps -axu command. The first "word" on a line is the owner of the job, and so grep "^ftp" extracts only the FTP processes. The ps -axu format puts the time or month as the 9th word on the line and the process Id as the second word. Hence the awk command selects the 24 or more hour old processes and outputs their process Identifiers. This set of Ids (the old ftp processes) are read in, one at a time by the while - do - done loop and killed.Clearly the only change is check for the presence of a ":" in the 9th word, extract the hour (when it started) and compare:

awk '$9!~/:/{print $2}

$9~/:/{S=substr($9,0,2);

if(S-T>=g || S-T<0 && (S-T+24)>g)print $2;

}' g=$grace T=`date +%H`

## Testing

There is a hopeful theory that a program that is properly developed does not need testing. Given the unprovable state of most software tools this is a dangerous theory. In this case testing showed up a bug caused by the weak typing in 'awk'. The correct statement to select outstanding jobs is:if(S-T>=0+g || S-T<0 && (S-T+24)>0+g)print $2;

since g is interpreted as a string and so lexographic rather than numeric ordering is used in the comparisons.## Conclusion

Notice that the condition was not wrong. It is the coding that fell into a well known and avoidable trap. - (above)|- (5.1): D%24=d%24,
- (r1, 5.1, ei, k=>k1, ei, k=>k2)|- (5.2): D+k1*24=d+24*k2,
- (5.2)|- (5.3): D= -k1*24+d+24*k2,
- (5.3)|- (5.4): D= d+24*(k2-k1),
- (5.4, eg, k=>k2-k1)|- (5.5): D= d+24*k,
# Proof of 11

Let

(Close Let )

# Proof of 15

Let

(Close Let )

# Proof of 18

Let

(Close Let )

# Notes

(ei): The "existential instanciation" rule of inference [ ei in logic_2_Proofs ]

(eg): The "existential generalization" rule of inference [ eg in logic_2_Proofs ]

My problem is to get a function that tells me whether or not a the difference between to 24-hour times is greater than a given grace period - when the times are available only as 24-hour times.

Let

*. . . . . . . . . ( end of section What jobs have been running too long) *<<Contents | End>>