Just a quick question, before I study the Poly/ML sources in detail.
What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there?
I have recently found by accident that I have hundreds of such files lying around. Maybe I just got some Poly/ML build/run options wrong, such that statistics are enabled accidentally.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the shared-memory file be for global stats only?
Makarius
On 27/06/2014 12:03, Makarius wrote:
What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there?
Poly/ML always creates a .polyml directory and a poly-stats file. The poly-stats file will be deleted when the Poly/ML process finishes normally. If it crashes, though, the file will remain.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the shared-memory file be for global stats only?
The Poly/ML process does not know when another process wants to read the statistics so they are always made available as a memory-mapped file.
David
On 27 Jun 2014, at 17:53, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 27/06/2014 12:03, Makarius wrote:
What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there?
Poly/ML always creates a .polyml directory and a poly-stats file. The poly-stats file will be deleted when the Poly/ML process finishes normally. If it crashes, though, the file will remain.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the shared-memory file be for global stats only?
The Poly/ML process does not know when another process wants to read the statistics so they are always made available as a memory-mapped file.
I discovered the same problem with ProofPower where users run via a GUI which just kills the ProofPower executable when the user quits or asks to restart the ProofPower session. It is a bit surprising that running a stand-alone program (like Joe Hurd?s opentheory or my slrp parser generator) creates $HOME/.polyml and that aborting a run with Ctrl+C leaves a stats file in that directory.
The files are only 4096 bytes so it is not much of an overhead, but it is a bit messy. Would it make sense to provide a function in PolyML.Statistics allowing a process to opt into making its statistics available? (Or conversely, is there a requirement to access statistics from a program that has not been designed with that in mind?)
Regards,
Rob.
On 29/06/2014 11:41, Rob Arthan wrote:
The files are only 4096 bytes so it is not much of an overhead, but it is a bit messy. Would it make sense to provide a function in PolyML.Statistics allowing a process to opt into making its statistics available? (Or conversely, is there a requirement to access statistics from a program that has not been designed with that in mind?)
The idea was to make the statistics available for another poly or a different program. The difficulty is finding a way to make them available. In Windows it is possible to have a named shared memory segment which is created by the poly process and can be opened, read-only, by another process. When the creating process finishes the memory segment is deleted unless another process is currently reading it. There's no equivalent, as far as I can tell, in Unix. The only way to make a shared memory segment available to another process is to map a file and the file will remain after the creating process exits unless it is explicitly deleted.
My preference would be for a way to have the equivalent of named shared memory segments. If there is no alternative to the present scheme of creating a mapped file in the file system then it would probably be better to only create it if the creating process explicitly requests it. That could be a flag somewhere in PolyML.Statistics or, probably easier, a command line option. Any ideas?
David
David,
On 2 Jul 2014, at 11:42, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 29/06/2014 11:41, Rob Arthan wrote:
The files are only 4096 bytes so it is not much of an overhead, but it is a bit messy. Would it make sense to provide a function in PolyML.Statistics allowing a process to opt into making its statistics available? (Or conversely, is there a requirement to access statistics from a program that has not been designed with that in mind?)
The idea was to make the statistics available for another poly or a different program. The difficulty is finding a way to make them available. In Windows it is possible to have a named shared memory segment which is created by the poly process and can be opened, read-only, by another process. When the creating process finishes the memory segment is deleted unless another process is currently reading it. There's no equivalent, as far as I can tell, in Unix. The only way to make a shared memory segment available to another process is to map a file and the file will remain after the creating process exits unless it is explicitly deleted.
My preference would be for a way to have the equivalent of named shared memory segments.
Have you looked at System V shared memory (shmget/shmat etc.)? This seems to be available on most flavours of UN*X these days. However, it is a long while since I have used these interfaces and they may just move the problem from the world of ls and rm to the world of ipcs and ipcrm.
If there is no alternative to the present scheme of creating a mapped file in the file system then it would probably be better to only create it if the creating process explicitly requests it. That could be a flag somewhere in PolyML.Statistics or, probably easier, a command line option. Any ideas?
If you stick with mmap, then control via the command line looks good to me.
Regards,
Rob.
On 02/07/2014 13:20, Rob Arthan wrote:
Have you looked at System V shared memory (shmget/shmat etc.)? This seems to be available on most flavours of UN*X these days. However, it is a long while since I have used these interfaces and they may just move the problem from the world of ls and rm to the world of ipcs and ipcrm.
Thanks for suggesting this. I was hoping someone might be able to suggest something. However, looking a bit more closely, I can see a problem. shmget uses a "key" which has to be derived from an existing file via ftok. That looks as though it would require a file to be created in the file system for each process. It could be zero size but I think it leads to the problem you've identified.
If there is no alternative to the present scheme of creating a mapped file in the file system then it would probably be better to only create it if the creating process explicitly requests it. That could be a flag somewhere in PolyML.Statistics or, probably easier, a command line option. Any ideas?
If you stick with mmap, then control via the command line looks good to me.
I'll have a think about this but it looks like it might be the best solution.
David
David,
On 2 Jul 2014, at 13:41, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 02/07/2014 13:20, Rob Arthan wrote:
Have you looked at System V shared memory (shmget/shmat etc.)? This seems to be available on most flavours of UN*X these days. However, it is a long while since I have used these interfaces and they may just move the problem from the world of ls and rm to the world of ipcs and ipcrm.
Thanks for suggesting this. I was hoping someone might be able to suggest something. However, looking a bit more closely, I can see a problem. shmget uses a "key" which has to be derived from an existing file via ftok. That looks as though it would require a file to be created in the file system for each process. It could be zero size but I think it leads to the problem you've identified.
I don?t think you have to use ftok (in fact, I have never used it). However you do need some scheme for allocating the numbers. I don?t know if you can arrange to have shared memory segments automatically disappear when all related processes die (which is why I thought you might just be moving the problem into a different namespace).
Regards,
Rob.
On Wed, 2 Jul 2014, David Matthews wrote:
Thanks for suggesting this. I was hoping someone might be able to suggest something. However, looking a bit more closely, I can see a problem. shmget uses a "key" which has to be derived from an existing file via ftok. That looks as though it would require a file to be created in the file system for each process. It could be zero size but I think it leads to the problem you've identified.
'Advanced Programming in the Unix Environment' by R. Stevens discusses the pros and cons of IPC with and without 'ftok'. Would be far too complicated to talk about this here.
Regards, Michael
On Wed, 2014-07-02 at 11:42 +0100, David Matthews wrote:
My preference would be for a way to have the equivalent of named shared memory segments. If there is no alternative to the present scheme of creating a mapped file in the file system then it would probably be better to only create it if the creating process explicitly requests it. That could be a flag somewhere in PolyML.Statistics or, probably easier, a command line option. Any ideas?
While I agree that leftover files in ~/.poly are not ideal, a benefit of the current solution is that it allows performance monitoring without explicit support from the monitored process.
How about POSIX shared memory (shm_open and related functions)? This should create files in /dev/shm on Linux. If I understand correctly, these will be removed automatically eventually (e.g., on reboot).
Alternatively, how about simply relocating the current files to /tmp?
Best, Tjark
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
mmoel＠t-online.de -
rda＠lemma-one.com -
tjark.weber＠gmx.de