arminbiere / runlim Goto Github PK
View Code? Open in Web Editor NEWLicense: Other
runlim's People
Contributors
Stargazers
Watchers
runlim's Issues
`can not open '%s' for reading` but subprocess not killed
For example, on MacOS:
ec2-user@[redacted] runlim % ./runlim --time-limit=4 ../minisat-v1.14/minisat ../minisat-v1.14/files/004b0f451f7d96f6a572e9e76360f51a-spg_420_280.cnf
[runlim] version: 2.0.0rc8
[runlim] time limit: 4 seconds
[runlim] real time limit: 311040000 seconds
[runlim] space limit: 16384 MB
[runlim] argv[0]: ../minisat-v1.14/minisat
[runlim] argv[1]: ../minisat-v1.14/files/004b0f451f7d96f6a572e9e76360f51a-spg_420_280.cnf
[runlim] start: Fri Sep 29 11:47:35 2023
[runlim] child: 75939
runlim error: can not open directory '/proc'
ec2-user@[redacted] runlim % ==================================[MINISAT]===================================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Clauses Literals | Limit Clauses Literals Lit/Cl | |
==============================================================================
| 0 | 3463100 11760316 | 1154366 0 0 nan | 0.000 % |
| 100 | 3463100 11760316 | 1269802 100 725 7.2 | 0.000 % |
| 252 | 3463100 11760316 | 1396782 252 1811 7.2 | 0.000 % |
| 477 | 3463104 11760316 | 1536461 473 3149 6.7 | 0.000 % |
| 814 | 3462352 11758391 | 1690107 762 19943 26.2 | 0.027 % |
I guess the subprocess has already been started, so error(1) at the end of open_proc_file_path_for_reading only kills runlim itself?
The time limit is not enforced, but that's expected, I think. Mac doesn't have /proc. It's kinda odd, I guess, maybe someone could think this would work on Mac but it doesn't ๐ข
Mate
Short option -r is not working
The short option -r is not working, which should be easy to fix:
--- a/runlim.c
+++ b/runlim.c
@@ -1285,6 +1285,7 @@ main (int argc, char **argv)
break;
case 's':
+ case 'r':
case 't':
i++;Configure delay between SIGTERM and SIGKILL
We have been using the runsolver tool in the past and would like to switch to runlim due to issues with the tool. We were using one particular feature of the runsolver that allows for setting a delay sending the SIGTERM and SIGKILL signals in case the system takes a little longer to shut down. As far as I can see, the delay between the two signals in runlim is hard coded.
Would it be possible to provide an option to configure this delay. So that after say n seconds a SIGTERM is send and after n+delay seconds a SIGKILL is sent?
need better group and session id handling
For some runs on a busy cluster it seems that it rarely occured that process identifiers wrap around and actually just from group or session to child pid, which then is smaller than either the sesssion or group identifier:
../6s196.err:runlim error: group pid 4190248 larger than child pid 4251
../6s1.err:runlim error: session pid 4180036 larger than child pid 10322
../beembrptwo1b2.err:runlim error: session pid 4180065 larger than child pid 10321
../beembrptwo4b1.err:runlim error: group pid 4180039 larger than child pid 4369
This breaks some logic in runlim to determine whether a process is in the same process group, which in turn is used to kill zombie process more reliable in the last major update of runlim. So this is tricky business to get right anyhow. I document it here but have no idea how to fix it yet.
Does not work correctly when the shell script terminates quick but subprocesses keep running
I just found a bug I think. Shell script:
#!/bin/bash
./cryptominisat complicated.cnf &
./cryptominisat complicated.cnf &
./cryptominisat complicated.cnf &
./cryptominisat complicated.cnf &
Then run as:
./runlim -t 10 ./myshell.sh
This will make runlim terminate immediately as if all was good. However, the 4 cryptominisat processes will keep running. I THINK this may be because it runs for less than 100ms and so runlim doesn't even do a single child check? Anyway, if I remove the last & then it correctly identifies all 4 subprocesses. Otherwise, all seems "fine and dandy" except that cryptominisat will keep running forever in 4 copies.
Output:
~/development/runlim ๎ฑ orig ?2 ๎ฐ ./runlim myshell.sh ๎ฒ โ ๎ณ 4s
[runlim] version: 2.0.0rc9
[runlim] host: tiresias
[runlim] time limit: 311040000 seconds
[runlim] real time limit: 311040000 seconds
[runlim] space limit: 64222 MB
[runlim] argv[0]: myshell.sh
[runlim] start: Wed Nov 8 02:23:19 2023
[runlim] child: 90605
[runlim] end: Wed Nov 8 02:23:19 2023
[runlim] status: ok
[runlim] result: 0
[runlim] children: 0
[runlim] processes: 93
[runlim] real: 0.01 seconds
[runlim] time: 0.00 seconds
[runlim] space: 0 MB
[runlim] load: 0.00 maximum
[runlim] samples: 0
But after this successful output we have:
~/development/runlim ๎ฑ orig ?2 ๎ฐ ps ๎ฒ โ
PID TTY TIME CMD
79593 pts/5 00:00:08 zsh
79597 pts/5 00:00:00 zsh
79664 pts/5 00:00:00 zsh
79666 pts/5 00:00:00 zsh
79667 pts/5 00:00:08 gitstatusd-linu
90606 pts/5 00:00:19 cryptominisat5
90607 pts/5 00:00:19 cryptominisat5
90608 pts/5 00:00:19 cryptominisat5
90609 pts/5 00:00:19 cryptominisat5
90622 pts/5 00:00:00 ps
And top is showing CryptoMiniSat running.
I would consider this a major bug, I think?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.