Вопрос или проблема
$ lsb_release -a
Нет доступных модулей LSB.
Идентификатор дистрибутива: Ubuntu
Описание: Ubuntu 20.04.6 LTS
Версия: 20.04
Кодовое имя: focal
$ uname -r
5.15.0-125-generic
Я пытаюсь работать с доказательным ассистентом по теоремам coq, установленным через snap, используя Emacs и proof general. К сожалению, я получил ошибку. После исследования с помощью strace я выяснил, что ошибка вызвана системным вызовом futex
“доступ запрещен”, когда программа пытается обработать файл в директории /tmp
:
$ strace coqdep /tmp/ProofGeneral-coqofYWUP.v
пытаюсь имитировать то, что делает proof general, и получил следующее:
--- SIGURG {si_signo=SIGURG, si_code=SI_TKILL, si_pid=123729, si_uid=1000} ---
rt_sigreturn({mask=[]}) = 22
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
getpid() = 123729
tgkill(123729, 123750, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
futex(0x55610de9d250, FUTEX_WAIT_PRIVATE, 0, {tv_sec=0, tv_nsec=100000}) = 0
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
getpid() = 123729
tgkill(123729, 123750, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
epoll_pwait(4, [], 128, 0, NULL, 0) = 0
futex(0xc000100948, FUTEX_WAKE_PRIVATE, 1) = 1
futex(0x55610de9d250, FUTEX_WAIT_PRIVATE, 0, {tv_sec=0, tv_nsec=100000}) = 0
close(3) = 0
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, 0, NULL, 0) = 1
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
epoll_pwait(4, [], 128, 0, NULL, 191668) = 0
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [{EPOLLIN|EPOLLOUT, {u32=1967093592, u64=140516117149528}}], 128, 0, NULL, 0) = 1
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
epoll_pwait(4, [], 128, 0, NULL, 191668) = 0
epoll_pwait(4, [{EPOLLIN|EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="l\2\1\1'\0\0\0l\4\0\0-\0\0\0", iov_len=16}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 16
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="\5\1u\0\2\0\0\0\6\1s\0\6\0\0\0:1.155\0\0\10\1g\0\1o\0\0"..., iov_len=48}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 48
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="\"\0\0\0/org/freedesktop/systemd1/jo"..., iov_len=39}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 39
futex(0xc000100948, FUTEX_WAKE_PRIVATE, 1) = 1
recvmsg(3, {msg_namelen=112}, MSG_CMSG_CLOEXEC) = -1 EAGAIN (Ресурс временно недоступен)
openat(AT_FDCWD, "/proc/123729/cgroup", O_RDONLY|O_CLOEXEC) = 8
epoll_ctl(4, EPOLL_CTL_ADD, 8, {EPOLLIN|EPOLLOUT|EPOLLRDHUP|EPOLLET, {u32=1967093592, u64=140516117149528}}) = -1 EPERM (Операция не разрешена)
read(8, "13:cpuset:/\n12:rdma:/\n11:memory:"..., 4096) = 547
close(8) = 0
write(6, "\0", 1) = 1
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [], 128, 0, NULL, 0) = 0
epoll_pwait(4, <незавершенная ...>) = ?
*** Ошибка: /tmp/ProofGeneral-coqofYWUP.v: Нет такого файла или директории
+++ завершено с 1 +++
-
К сожалению, я не обладаю достаточной квалификацией, чтобы понять, что вызывает доступ запрещен для системного вызова. Я даже установил разрешения 777 для этого файла, это не помогло.
-
После того как я скопировал файл в свою домашнюю директорию, он начал работать:
$ cp /tmp/ProofGeneral-coqofYWUP.v ~/aaa.v
$ coqdep ~/aaa.v
home/usr345/aaa.vo /home/usr345/aaa.glob /home/usr345/aaa.v.beautified /home/usr345/aaa.required_vo: /home/usr345/aaa.v
/home/usr345/aaa.vio: /home/usr345/aaa.v
Ответ или решение
Ошибка "futex for a file in /tmp directory: operation not permitted" в Ubuntu 20.04
В данном материале мы подробно рассмотриваем ошибку, возникающую при попытке работы с файлом в каталоге /tmp
в среде Ubuntu 20.04. Эта проблема может иметь несколько причин, и важно её поймать, чтобы обеспечить нормальную работу приложения, в данном случае — Coq, установленного через Snap.
Описание проблемы
Вы пытаетесь запустить команду coqdep
, которая необходима для работы с файлом /tmp/ProofGeneral-coqofYWUP.v
, однако получаете ошибку Operation not permitted
при вызове системного вызова futex
. Анализ с использованием strace
показывает, что проблема возникает в результате недоступности ресурса, связанного с группами контроля (cgroups), особенно при выполнении следующих строк:
epoll_ctl(4, EPOLL_CTL_ADD, 8, {EPOLLIN|EPOLLOUT|EPOLLRDHUP|EPOLLET, ...}) = -1 EPERM (Operation not permitted)
Это указывает на то, что приложение пытается выполнить операцию, не имея на это необходимых прав.
Причины возникновения ошибки
-
Проблемы прав доступа: Несмотря на то что вы установили права доступа 777 на файл, это может не воздействовать на ограничения, налагаемые системными настройками или политиками безопасности, в основном отвечающими за изоляцию приложений, установленных через Snap.
-
Изоляция Snap: Приложения, работающие в рамках системы Snap, часто имеют ограничения на доступ к файловым системам и ресурсам. Snap использует строгую модель изоляции, которая может препятствовать работе с файлами в каталоге
/tmp
. -
Контейнеризация: Ваша среда может быть настроена таким образом, что выполнение системных вызовов, которые требуют доступа к ресурсам за пределами контейнера или ограниченной системы, не допускается.
Решения проблемы
-
Перемещение файла: Как вы уже заметили, копирование файла из
/tmp
в ваш домашний каталог решает проблему. Это происходит потому, что ваш пользователь имеет полные права на доступ к директории вашего домашнего каталога, где отсутствуют ограничения, наложенные Snap.cp /tmp/ProofGeneral-coqofYWUP.v ~/aaa.v coqdep ~/aaa.v
-
Запуск Coq вне Snap: Если это возможно, рассмотрите запуск Coq без использования Snap, так как это может снизить уровень изоляции и разрешить необходимые разрешения.
-
Настройка системы: Если необходимо сохранить использование Snap, рассмотрите возможность изменения настроек конфигурации Snap или использование интерфейсов безопасности, позволяющих Coq получать доступ к определенным ресурсам.
-
Изменение прав доступа на уровень системы: Проверьте наличие других правовых или программных ограничений для
snapd
и конфигураций, связанных с cgroups. Инструменты управления такими системами могут помочь в этом процессе.
Заключение
Ошибки, подобные operation not permitted
, часто возникают в средах с высокой степенью изоляции, как Snap. Ключом к их решению является тщательное понимание контекста выполнения программ и ограничений, накладываемых системой. Перемещение файлов в домашний каталог является наиболее простым и эффективным методом обхода данной проблемы. Если дальнейшие проблемы сохраняются, полезно также обратиться к документированию Snap или сообществу для уточнения об установленных ограничениях.