Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

protect against SANY race conditions on the filesystem #3046

Merged
merged 8 commits into from
Dec 13, 2024
Merged

Conversation

konnov
Copy link
Collaborator

@konnov konnov commented Dec 13, 2024

Although rare, it may still happen that multiple CLI instances of Apalache hit concurrency issues that is filed in tlaplus/tlaplus#688 (apalache-mc server has a separate mutex for that):

$ cat t.tla
------------------- MODULE t --------------------                               
EXTENDS Integers
VARIABLE
    \* @type: Int;
    x
Init == x = 0
Next == x' = x + 1
=================================================
$ seq 1 100 | parallel ~/devl/apalache/bin/apalache-mc parse --out-dir=c/{} t.tla
...
Encountered an exception while attempt to validate /var/folders/93/s11lf4f16c77bpq91r90njbm0000gn/T/Naturals.tla - /var/folders/93/s11lf4f16c77bpq91r90njbm0000gn/T/Naturals.tla (No such file or directory)

This is a simple fix that was already discussed in tlaplus/tlaplus#688. We simply set java.io.tmpdir to a specific directory.

Actually, it seems like we have fixed it in #1959, but the above test shows otherwise.

@konnov konnov requested a review from thpani December 13, 2024 16:28
@konnov konnov requested a review from Kukovec December 13, 2024 16:31
@konnov konnov enabled auto-merge December 13, 2024 16:34
TMPDIR="$(pwd)/tmp"
mkdir -p "$TMPDIR"
fi
JAVA_IO_TMPDIR=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX`
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not skip -p (and the above) and rely on it's default behavior:

-p temp-dir, --tmpdir=temp-dir
              temp  directory  for  the  file.  This option is a member of the
              tmpdir class of options.

              If this option is not provided, mktemp will use the  environment
              variable  TMPDIR to find a suitable directory.  If these are not
              available, it will fall back to ~/tmp  or  /tmp.   A  <file-pat>
              command line argument containing a directory component will con-
              flict with this option.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For some reason, it does not work with docker this way. Maybe it's using nix and it has different behavior. But it does not even work with my fix.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The above test was failing due to extra protection flags, now using ${TMPDIR:-}. This works. Let me see how it works without -p. It definitely did not work without the additional test for TMPDIR above

@thpani thpani disabled auto-merge December 13, 2024 17:26
Copy link
Collaborator

@thpani thpani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have one question (see above), so I've disabled auto-merge.

But in general, LGTM

@konnov konnov merged commit 1742832 into main Dec 13, 2024
10 checks passed
@konnov konnov deleted the igor/tmpdir branch December 13, 2024 18:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants