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

- (The|-symbol is used to indicate that a formaula has been asserted to be
true. It may be preceeded by a list of reasons.)
We can show that

- (mod)|- (r0): For i,j>0, i=i%j+j*(i/j).
- (mod)|- (r1): For i,j>0, for some k(i=k*j+i%j)).

Net- 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, now, on the 24 hour clock.
- g::0..23=the grace period in hours.
- D::int=T-S, the difference between to 24 hour clock times.
- d::int=t-s, the real time difference in hours.
Given D and g we want to determine if d > g or if d<=g.

We have been told:

- (given)|- (1): T = t % 24
- (given)|- (2): S = s % 24
- (given)|- (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).
## Proof of 5

Let- (4)|- (5.0): (T-S)%24 = (t-s)%24.
- (5.0, D, d)|- (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,

(Close Let )

## Proof of 11

Let

(Close Let )

## Proof of 15

Let

(Close Let )

## Proof of 18

Let

(Close Let )

- (4)|- (5.0): (T-S)%24 = (t-s)%24.

(End of Net)

## C and C++ Code

We would therefore use the following functionint hangable(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. - given::=a reason for assuming something.
- above::=short hand for using all previous assertions as the reason for the next one.

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

Use C.expressions. (above) |-(mod): For int i,j>0, i%j::=i - j*(i/j).

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

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

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