support for timing of the managed process;

--- a/Admin/bash_process/bash_process.c	Wed Mar 09 13:12:51 2016 +0100
+++ b/Admin/bash_process/bash_process.c	Wed Mar 09 13:33:21 2016 +0100
@@ -3,11 +3,14 @@
 Bash process with separate process group id.
 */
 
+#include <stdio.h>
 #include <stdlib.h>
-#include <stdio.h>
 #include <string.h>
+#include <sys/resource.h>
+#include <sys/time.h>
 #include <sys/types.h>
 #include <sys/wait.h>
+#include <time.h>
 #include <unistd.h>
 
 static void fail(const char *msg)
@@ -22,26 +25,48 @@
 {
   /* args */
 
-  if (argc < 2) {
-    fprintf(stderr, "Bad arguments: missing pid file\n");
+  if (argc < 3) {
+    fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
     fflush(stderr);
     exit(1);
   }
   char *pid_name = argv[1];
+  char *timing_name = argv[2];
 
 
-  /* setsid */
+  /* potential fork */
 
-  if (setsid() == -1) {
+  time_t time_start = time(NULL);
+
+  if (strlen(timing_name) > 0 || setsid() == -1) {
     pid_t pid = fork();
-    int status;
 
     if (pid == -1) fail("Cannot set session id (failed to fork)");
     else if (pid != 0) {
+      int status;
+
       if (waitpid(pid, &status, 0) == -1) {
         fail("Cannot join forked process");
       }
 
+      /* report timing */
+
+      if (strlen(timing_name) > 0) {
+        long long timing_elapsed = (time(NULL) - time_start) * 1000;
+
+        struct rusage ru;
+        getrusage(RUSAGE_CHILDREN, &ru);
+
+        long long timing_cpu =
+          ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
+          ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
+
+        FILE *timing_file = fopen(timing_name, "w");
+        if (timing_file == NULL) fail("Cannot open timing file");
+        fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
+        fclose(timing_file);
+      }
+
       if (WIFEXITED(status)) {
         exit(WEXITSTATUS(status));
       }
@@ -74,9 +99,10 @@
   /* shift command line */
 
   int i;
-  for (i = 2; i < argc; i++) {
-    argv[i - 2] = argv[i];
+  for (i = 3; i < argc; i++) {
+    argv[i - 3] = argv[i];
   }
+  argv[argc - 3] = NULL;
   argv[argc - 2] = NULL;
   argv[argc - 1] = NULL;