search

arminbiere / runlim

Other
12 stars 4 forks source link

`can not open '%s' for reading` but subprocess not killed #6

Open msooseth opened 9 months ago

msooseth commented 9 months ago

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 :cry:

Mate

arminbiere commented 9 months ago

Yep, I was just fuzzing (with mobical) on MacOS and did not wrap it into runlim.

Probably there is similar functionality on MacOS though. For instances in kissat I found a way to determine current resident set size on MacOS (see resources.c) instead of going through /proc, but that is not well document (the Internet knows though)..

To port runlim completely to MacOS one would need to find a way to traverse the process tree (well ps also exists on MacOS and was used as inspiration for runlim on Linux too). Maybe if my Apple HW is more powerful than my Indel/AMD machines I will look into that.

msooseth commented 9 months ago

Yeah, it's possible via sysctl apparently on MacOS. But I don't feel like re-writing much of runlim for sysctl. Currently, I'm just going to run it inside Docker, which runs inside a Linux VM. Sad, but at least it works. BTW, the MacOS hardware is insanely good. There is a Linux distro for it too, https://asahilinux.org/

arminbiere commented 9 months ago

Well my AMD machines are faster (30% than my M2 Pro) and have more cores (but also need way more power).