Admin/bash_process/bash_process.c
author wenzelm
Wed, 16 Mar 2016 22:19:08 +0100
changeset 62645 a2351f82bc48
parent 62575 590df5f4e531
permissions -rw-r--r--
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     1
/*  Author:     Makarius
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     2
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
     3
Bash process with separate process group id.
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     4
*/
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     5
62575
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
     6
#include <signal.h>
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
     7
#include <stdio.h>
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     8
#include <stdlib.h>
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
     9
#include <string.h>
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    10
#include <sys/resource.h>
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    11
#include <sys/time.h>
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    12
#include <sys/types.h>
62300
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    13
#include <sys/wait.h>
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    14
#include <time.h>
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    15
#include <unistd.h>
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    16
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    17
static void fail(const char *msg)
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    18
{
47798
03ab3bd78282 print errors on stderr;
wenzelm
parents: 47797
diff changeset
    19
  fprintf(stderr, "%s\n", msg);
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
    20
  fflush(stderr);
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    21
  exit(2);
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    22
}
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    23
62568
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    24
static time_t now()
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    25
{
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    26
  struct timeval tv;
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    27
  if (gettimeofday(&tv, NULL) == 0) {
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    28
    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    29
  }
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    30
  else {
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    31
    return time(NULL) * 1000;
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    32
  }
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    33
}
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    34
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    35
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    36
int main(int argc, char *argv[])
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    37
{
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    38
  /* args */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    39
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    40
  if (argc < 3) {
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    41
    fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
    42
    fflush(stderr);
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    43
    exit(1);
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    44
  }
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    45
  char *pid_name = argv[1];
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    46
  char *timing_name = argv[2];
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    47
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    48
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    49
  /* potential fork */
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    50
62568
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    51
  time_t time_start = now();
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    52
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    53
  if (strlen(timing_name) > 0 || setsid() == -1) {
50290
735bea8d89c9 more defensive retry via fork;
wenzelm
parents: 49551
diff changeset
    54
    pid_t pid = fork();
62300
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    55
50290
735bea8d89c9 more defensive retry via fork;
wenzelm
parents: 49551
diff changeset
    56
    if (pid == -1) fail("Cannot set session id (failed to fork)");
62300
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    57
    else if (pid != 0) {
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    58
      int status;
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    59
62575
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    60
      // ingore SIGINT
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    61
      struct sigaction sa;
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    62
      memset(&sa, 0, sizeof(sa));
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    63
      sa.sa_handler = SIG_IGN;
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    64
      sigaction(SIGINT, &sa, 0);
590df5f4e531 ignore SIGINT in waiting wrapper process;
wenzelm
parents: 62568
diff changeset
    65
62300
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    66
      if (waitpid(pid, &status, 0) == -1) {
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    67
        fail("Cannot join forked process");
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    68
      }
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    69
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    70
      /* report timing */
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    71
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    72
      if (strlen(timing_name) > 0) {
62568
3541bc1e97d2 elapsed time in milliseconds (cf. Time.now in Poly/ML);
wenzelm
parents: 62567
diff changeset
    73
        long long timing_elapsed = now() - time_start;
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    74
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    75
        struct rusage ru;
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    76
        getrusage(RUSAGE_CHILDREN, &ru);
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    77
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    78
        long long timing_cpu =
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    79
          ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    80
          ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    81
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    82
        FILE *timing_file = fopen(timing_name, "w");
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    83
        if (timing_file == NULL) fail("Cannot open timing file");
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    84
        fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    85
        fclose(timing_file);
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    86
      }
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
    87
62300
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    88
      if (WIFEXITED(status)) {
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    89
        exit(WEXITSTATUS(status));
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    90
      }
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    91
      else if (WIFSIGNALED(status)) {
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    92
        exit(128 + WTERMSIG(status));
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    93
      }
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    94
      else {
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    95
        fail("Unknown status of forked process");
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    96
      }
f41884b9c4f1 actually wait for forked process and return its status -- this is not meant to be a daemon;
wenzelm
parents: 62293
diff changeset
    97
    }
50290
735bea8d89c9 more defensive retry via fork;
wenzelm
parents: 49551
diff changeset
    98
    else if (setsid() == -1) fail("Cannot set session id (after fork)");
735bea8d89c9 more defensive retry via fork;
wenzelm
parents: 49551
diff changeset
    99
  }
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
   100
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
   101
50292
45fe12c9788e report proper pid *after* fork;
wenzelm
parents: 50290
diff changeset
   102
  /* report pid */
45fe12c9788e report proper pid *after* fork;
wenzelm
parents: 50290
diff changeset
   103
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   104
  if (strcmp(pid_name, "-") == 0) {
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   105
    fprintf(stdout, "%d\n", getpid());
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   106
    fflush(stdout);
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   107
  }
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   108
  else if (strlen(pid_name) > 0) {
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   109
    FILE *pid_file;
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   110
    pid_file = fopen(pid_name, "w");
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   111
    if (pid_file == NULL) fail("Cannot open pid file");
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   112
    fprintf(pid_file, "%d", getpid());
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   113
    fclose(pid_file);
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   114
  }
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   115
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   116
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   117
  /* shift command line */
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   118
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   119
  int i;
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
   120
  for (i = 3; i < argc; i++) {
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
   121
    argv[i - 3] = argv[i];
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   122
  }
62567
cb4e6ca06505 support for timing of the managed process;
wenzelm
parents: 62300
diff changeset
   123
  argv[argc - 3] = NULL;
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   124
  argv[argc - 2] = NULL;
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   125
  argv[argc - 1] = NULL;
50292
45fe12c9788e report proper pid *after* fork;
wenzelm
parents: 50290
diff changeset
   126
45fe12c9788e report proper pid *after* fork;
wenzelm
parents: 50290
diff changeset
   127
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
   128
  /* exec */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
   129
62292
486236dcd4d7 more flexible command-line;
wenzelm
parents: 50292
diff changeset
   130
  execvp("bash", argv);
47796
c37411691ee7 more direct exec with synchronous exit code;
wenzelm
parents: 47764
diff changeset
   131
  fail("Cannot exec process");
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
   132
}