From 7b7a946485bbb1f918cc0555e05f10c573ff551f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 4 Jun 2012 16:38:42 +0200 Subject: [PATCH] Rework the timeout of the CGI script. The previous implementation was fine to catch timeout of third-party tools (like dot), but to good to catch timeout in Spot itself, because Python will not deliver a SIGALRM while a native function (e.g. Spot's translation) is running. So we fork() the Python process, with a parent that does nothing but wait for the termination of the child or for an alarm. On SIGALRM, the parent kills all children. * wrap/python/ajax/spot.in: Adjust to fork. * wrap/python/tests/alarm.py: New test file to test this scenario in a more controled environment. * wrap/python/tests/Makefile.am: Add it. --- NEWS | 4 ++- wrap/python/ajax/spot.in | 20 +++++++---- wrap/python/tests/Makefile.am | 1 + wrap/python/tests/alarm.py | 68 +++++++++++++++++++++++++++++++++++ 4 files changed, 86 insertions(+), 7 deletions(-) create mode 100755 wrap/python/tests/alarm.py diff --git a/NEWS b/NEWS index 300514117..3d7e93dd3 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 0.9.1a: - Nothing yet. + * Bug fixes: + - The CGI script running for ltl2tgba.html will correctly timeout + after 30s when Spot's translation takes more time. New in spot 0.9.1 (2012-05-23): diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 722c2fe92..e2732788f 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -220,16 +220,12 @@ If you want to benchmark big formulae it is better to install Spot on your own computer.

\n""") finish(kill = True) -def reset_alarm(): - signal.alarm(30) - def run_dot(basename, ext): outname = basename + '.' + ext # Do not call "dot" to generate a file that already exists. if not os.access(outname, os.F_OK): os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext, '-Gsize=8.2,8.2', '-o', outname, basename + '.txt') - reset_alarm() # Create a unused hardlink that points to the output picture # just to remember how many cache entries are sharing it. os.link(outname, tmpdir + "/" + ext) @@ -344,8 +340,20 @@ if output_type == 'v': spot.unblock_signal(signal.SIGALRM) spot.unblock_signal(signal.SIGTERM) os.setpgrp() -signal.signal(signal.SIGALRM, alarm_handler) -reset_alarm() + +child = os.fork() +if child != 0: + # In parent. We are just waiting for the termination of the + # child, or for the timeout alarm. On SIGALRM, we will kill the + # child. + # + # We cannot avoid forking, because Python will not deliver a + # signal when a C function is running. So if Spot takes too long + # to translate some formula, it would not get interrupted. + signal.signal(signal.SIGALRM, alarm_handler) + signal.alarm(30) + os.waitpid(child, 0) + exit(0) # Global options utf8 = False diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index c1dddb471..406cf1a7e 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -30,6 +30,7 @@ TESTS_ENVIRONMENT = ./run check_SCRIPTS = run TESTS = \ + alarm.py \ ltlsimple.py \ ltlparse.py \ bddnqueen.py \ diff --git a/wrap/python/tests/alarm.py b/wrap/python/tests/alarm.py new file mode 100755 index 000000000..1fa739bef --- /dev/null +++ b/wrap/python/tests/alarm.py @@ -0,0 +1,68 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2012 Laboratoire de Recherche et Développement +# de l'Epita +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +import spot +import time +import signal +import sys +import os + +def alarm_handler(signum, frame): + sys.stdout.write("signaled\n") + os.kill(child, signal.SIGTERM) + exit(0) + +f = """!(G(F(P_Rbt2.observe)&& F(P_Rbt3.observe) && +F(P_rbt1.observe)&& F(P_Rbt1.plus || P_Rbt1.moins || P_Rbt1.stop)&& +F(P_Rbt3.plus || P_Rbt3.moins || P_Rbt3.stop) && F(P_Rbt2.plus || +P_Rbt2.moins || P_Rbt2.stop))-> G((F "map[0]==1") && (F "map[1]==1") +&& (F "map[2]==1") && (F "map[3]==1") && (F "map[4]==1") && (F +"map[5]==1") && (F "map[6]==1") && (F "map[7]==1") && (F "map[8]==1") +&& (F "map[9]==1") && (F "map[0]==2") && (F "map[1]==2") && (F +"map[2]==2") && (F "map[3]==2") && (F "map[4]==2") && (F "map[5]==2") +&& (F "map[6]==2") && (F "map[7]==2") && (F "map[8]==2") && (F +"map[9]==2") && (F "map[0]==3") && (F "map[1]==3") && (F "map[2]==3") +&& (F "map[3]==3") && (F "map[4]==3") && (F "map[5]==3") && (F +"map[6]==3") && (F "map[7]==3") && (F "map[8]==3") && (F +"map[9]==3")))""" + +e = spot.default_environment.instance() +p = spot.empty_parse_error_list() +f = spot.parse(f, p, e) +d = spot.bdd_dict() + +spot.unblock_signal(signal.SIGALRM) +spot.unblock_signal(signal.SIGTERM) +os.setpgrp() +child = os.fork() +if child != 0: + signal.signal(signal.SIGALRM, alarm_handler) + signal.alarm(2) + os.waitpid(child, 0) + # If the child returns, before we get the alarm it's a bug. + exit(1) + +# This is expected to take WAY more that 2s. +print "Before" +spot.ltl_to_tgba_fm(f, d, True) +print "After" + +exit(1)