Skip to content

Commit

Permalink
basic signal handling: allow user to request a timeout (#32)
Browse files Browse the repository at this point in the history
  • Loading branch information
guykatzz authored May 8, 2018
1 parent bc37160 commit 8e15b7a
Show file tree
Hide file tree
Showing 9 changed files with 155 additions and 1 deletion.
1 change: 1 addition & 0 deletions regress/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ SOURCES += \
Error.cpp \
FloatUtils.cpp \
MString.cpp \
SignalHandler.cpp \
TimeUtils.cpp \
\
AcasNeuralNetwork.cpp \
Expand Down
54 changes: 54 additions & 0 deletions src/common/SignalHandler.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
/********************* */
/*! \signalHandler SignalHandler.h
** \verbatim
** Top contributors (to current version):
** Guy Katz
** This signalHandler is part of the Marabou project.
** Copyright (c) 2016-2017 by the authors listed in the signalHandler AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the signalHandler COPYING in the top-level source
** directory for licensing information.\endverbatim
**/

#include "SignalHandler.h"
#include <cstring>
#include <signal.h>

void got_signal( int signalNumber )
{
SignalHandler::getInstance()->signalReceived( signalNumber );
}

SignalHandler *SignalHandler::getInstance()
{
static SignalHandler handler;
return &handler;
}

void SignalHandler::registerClient( Signalable *client )
{
_clients.append( client );
}

void SignalHandler::initialize()
{
struct sigaction sa;
memset( &sa, 0, sizeof(sa) );
sa.sa_handler = got_signal;
sigfillset( &sa.sa_mask );
sigaction( SIGQUIT, &sa, NULL );
}

void SignalHandler::signalReceived( unsigned /* signalNumber */ )
{
for ( const auto &signalable : _clients )
signalable->quitSignal();
}

//
// Local Variables:
// compile-command: "make -C ../.. "
// tags-signalHandler-name: "../../TAGS"
// c-basic-offset: 4
// End:
//
65 changes: 65 additions & 0 deletions src/common/SignalHandler.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
/********************* */
/*! \file SignalHandler.h
** \verbatim
** Top contributors (to current version):
** Guy Katz
** This file is part of the Marabou project.
** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**/

#ifndef __SignalHandler_h__
#define __SignalHandler_h__

#include "List.h"

class SignalHandler
{
public:
class Signalable
{
public:
virtual void quitSignal() = 0;
};

/*
Get the singleton signal handler
*/
static SignalHandler *getInstance();

/*
Register a client to receive signals
*/
void registerClient( Signalable *client );

/*
Initialize the signal handling
*/
void initialize();

/*
Called when a signal is received
*/
void signalReceived( unsigned signalNumber );

private:
List<Signalable *> _clients;

/*
Prevent additional instantiations of the class
*/
SignalHandler() {}
SignalHandler( const SignalHandler & ) {}
};

#endif // __SignalHandler_h__

//
// Local Variables:
// compile-command: "make -C ../.. "
// tags-file-name: "../../TAGS"
// c-basic-offset: 4
// End:
//
19 changes: 19 additions & 0 deletions src/engine/Engine.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ Engine::Engine()
, _basisRestorationRequired( Engine::RESTORATION_NOT_NEEDED )
, _basisRestorationPerformed( Engine::NO_RESTORATION_PERFORMED )
, _costFunctionManager( _tableau )
, _quitRequested( false )
{
_smtCore.setStatistics( &_statistics );
_tableau->setStatistics( &_statistics );
Expand Down Expand Up @@ -68,6 +69,9 @@ void Engine::adjustWorkMemorySize()

bool Engine::solve()
{
SignalHandler::getInstance()->initialize();
SignalHandler::getInstance()->registerClient( this );

storeInitialEngineState();

printf( "\nEngine::solve: Initial statistics\n" );
Expand All @@ -81,6 +85,16 @@ bool Engine::solve()
_statistics.addTimeMainLoop( TimeUtils::timePassed( mainLoopStart, mainLoopEnd ) );
mainLoopStart = mainLoopEnd;

if ( _quitRequested )
{
printf( "\n\nEngine: quitting due to external request...\n\n" );
printf( "Final statistics:\n" );
_statistics.print();

// Todo: return a separate exit code for tiemouts
return false;
}

try
{
DEBUG( _tableau->verifyInvariants() );
Expand Down Expand Up @@ -993,6 +1007,11 @@ void Engine::checkBoundCompliancyWithDebugSolution()
}
}

void Engine::quitSignal()
{
_quitRequested = true;
}

//
// Local Variables:
// compile-command: "make -C ../.. "
Expand Down
13 changes: 12 additions & 1 deletion src/engine/Engine.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
#include "Map.h"
#include "PrecisionRestorer.h"
#include "Preprocessor.h"
#include "SignalHandler.h"
#include "SmtCore.h"
#include "Statistics.h"

Expand All @@ -33,7 +34,7 @@ class InputQuery;
class PiecewiseLinearConstraint;
class String;

class Engine : public IEngine
class Engine : public IEngine, public SignalHandler::Signalable
{
public:
Engine();
Expand Down Expand Up @@ -66,6 +67,11 @@ class Engine : public IEngine
void restoreState( const EngineState &state );
void setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints );

/*
A request from the user to terminate
*/
void quitSignal();

const Statistics *getStatistics() const;

private:
Expand Down Expand Up @@ -181,6 +187,11 @@ class Engine : public IEngine
*/
AutoCostFunctionManager _costFunctionManager;

/*
Indicates a user request to quit
*/
bool _quitRequested;

/*
Perform a simplex step: compute the cost function, pick the
entering and leaving variables and perform a pivot.
Expand Down
1 change: 1 addition & 0 deletions src/engine/tests/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ SOURCES += \
Error.cpp \
FloatUtils.cpp \
MString.cpp \
SignalHandler.cpp \
TimeUtils.cpp \
\
BasisFactorizationFactory.cpp \
Expand Down
1 change: 1 addition & 0 deletions src/input_parsers/acas_example/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ SOURCES += \
Error.cpp \
FloatUtils.cpp \
MString.cpp \
SignalHandler.cpp \
TimeUtils.cpp \
\
BasisFactorizationFactory.cpp \
Expand Down
1 change: 1 addition & 0 deletions src/input_parsers/berkeley_example/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ SOURCES += \
FloatUtils.cpp \
HeapData.cpp \
MString.cpp \
SignalHandler.cpp \
TimeUtils.cpp \
\
BasisFactorizationFactory.cpp \
Expand Down
1 change: 1 addition & 0 deletions src/input_parsers/mps_generic/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ SOURCES += \
Equation.cpp \
FloatUtils.cpp \
MString.cpp \
SignalHandler.cpp \
TimeUtils.cpp \
\
BasisFactorizationFactory.cpp \
Expand Down

0 comments on commit 8e15b7a

Please sign in to comment.