Admin/bash_process/bash_process.c
author wenzelm
Fri Nov 03 19:20:47 2017 +0100 (19 months ago)
changeset 66997 17eb23e43630
parent 62575 590df5f4e531
permissions -rw-r--r--
avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
     1 /*  Author:     Makarius
     2 
     3 Bash process with separate process group id.
     4 */
     5 
     6 #include <signal.h>
     7 #include <stdio.h>
     8 #include <stdlib.h>
     9 #include <string.h>
    10 #include <sys/resource.h>
    11 #include <sys/time.h>
    12 #include <sys/types.h>
    13 #include <sys/wait.h>
    14 #include <time.h>
    15 #include <unistd.h>
    16 
    17 static void fail(const char *msg)
    18 {
    19   fprintf(stderr, "%s\n", msg);
    20   fflush(stderr);
    21   exit(2);
    22 }
    23 
    24 static time_t now()
    25 {
    26   struct timeval tv;
    27   if (gettimeofday(&tv, NULL) == 0) {
    28     return tv.tv_sec * 1000 + tv.tv_usec / 1000;
    29   }
    30   else {
    31     return time(NULL) * 1000;
    32   }
    33 }
    34 
    35 
    36 int main(int argc, char *argv[])
    37 {
    38   /* args */
    39 
    40   if (argc < 3) {
    41     fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
    42     fflush(stderr);
    43     exit(1);
    44   }
    45   char *pid_name = argv[1];
    46   char *timing_name = argv[2];
    47 
    48 
    49   /* potential fork */
    50 
    51   time_t time_start = now();
    52 
    53   if (strlen(timing_name) > 0 || setsid() == -1) {
    54     pid_t pid = fork();
    55 
    56     if (pid == -1) fail("Cannot set session id (failed to fork)");
    57     else if (pid != 0) {
    58       int status;
    59 
    60       // ingore SIGINT
    61       struct sigaction sa;
    62       memset(&sa, 0, sizeof(sa));
    63       sa.sa_handler = SIG_IGN;
    64       sigaction(SIGINT, &sa, 0);
    65 
    66       if (waitpid(pid, &status, 0) == -1) {
    67         fail("Cannot join forked process");
    68       }
    69 
    70       /* report timing */
    71 
    72       if (strlen(timing_name) > 0) {
    73         long long timing_elapsed = now() - time_start;
    74 
    75         struct rusage ru;
    76         getrusage(RUSAGE_CHILDREN, &ru);
    77 
    78         long long timing_cpu =
    79           ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
    80           ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
    81 
    82         FILE *timing_file = fopen(timing_name, "w");
    83         if (timing_file == NULL) fail("Cannot open timing file");
    84         fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
    85         fclose(timing_file);
    86       }
    87 
    88       if (WIFEXITED(status)) {
    89         exit(WEXITSTATUS(status));
    90       }
    91       else if (WIFSIGNALED(status)) {
    92         exit(128 + WTERMSIG(status));
    93       }
    94       else {
    95         fail("Unknown status of forked process");
    96       }
    97     }
    98     else if (setsid() == -1) fail("Cannot set session id (after fork)");
    99   }
   100 
   101 
   102   /* report pid */
   103 
   104   if (strcmp(pid_name, "-") == 0) {
   105     fprintf(stdout, "%d\n", getpid());
   106     fflush(stdout);
   107   }
   108   else if (strlen(pid_name) > 0) {
   109     FILE *pid_file;
   110     pid_file = fopen(pid_name, "w");
   111     if (pid_file == NULL) fail("Cannot open pid file");
   112     fprintf(pid_file, "%d", getpid());
   113     fclose(pid_file);
   114   }
   115 
   116 
   117   /* shift command line */
   118 
   119   int i;
   120   for (i = 3; i < argc; i++) {
   121     argv[i - 3] = argv[i];
   122   }
   123   argv[argc - 3] = NULL;
   124   argv[argc - 2] = NULL;
   125   argv[argc - 1] = NULL;
   126 
   127 
   128   /* exec */
   129 
   130   execvp("bash", argv);
   131   fail("Cannot exec process");
   132 }