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