Re: [polyml] Update to ARM code-generator

[David Matthews]

I've pushed some more updates to git master.  These are mostly 
improvements to the code, particularly floating point, but there are 
some fixes to bugs that could have produced bus errors or segmentation 
faults.


David

On 17/01/2022 23:44, Michael Norrish via polyml wrote:

I’m getting random SIGSEGVs while building HOL with latest git on an Apple 
Silicon MacBook Pro.  These don’t always occur, but when they do, they have (so 
far) always been in one of two places.

Michael


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Update to ARM code-generator

[Makarius]

On 16/01/2022 12:51, David Matthews wrote:
The long-promised update to the ARM code-generator is now in Git master.  This 
builds on the old version by adding the register allocation strategy borrowed 
from the X86 version as well as low-level peephole optimisation.  On my Apple 
M1 processor it now seems to be faster than X86 code with Rosetta.


There are still some improvements to be made, particularly with floating 
point, but no major changes are anticipated.  It includes one optimisation 
that isn't present on the X86 at the moment: small tuples are returned in 
registers rather than on the stack.


This is really great.

I have now started to make some tests with Isabelle + AFP, and will come back 
eventually with reports (and potential problems).



Makarius

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Update to ARM code-generator

[Michael Norrish via polyml]

I’m getting random SIGSEGVs while building HOL with latest git on an Apple 
Silicon MacBook Pro.  These don’t always occur, but when they do, they have (so 
far) always been in one of two places.

Michael

> On 16 Jan 2022, at 10:51 pm, David Matthews  
> wrote:
> 
> The long-promised update to the ARM code-generator is now in Git master.  
> This builds on the old version by adding the register allocation strategy 
> borrowed from the X86 version as well as low-level peephole optimisation.  On 
> my Apple M1 processor it now seems to be faster than X86 code with Rosetta.
> 
> There are still some improvements to be made, particularly with floating 
> point, but no major changes are anticipated.  It includes one optimisation 
> that isn't present on the X86 at the moment: small tuples are returned in 
> registers rather than on the stack.
> 
> Please try it and let me know how it goes.
> 
> David
> 
> ___
> polyml mailing list
> polyml@inf.ed.ac.uk
> https://aus01.safelinks.protection.outlook.com/?url=http%3A%2F%2Flists.inf.ed.ac.uk%2Fmailman%2Flistinfo%2Fpolymldata=04%7C01%7Cmichael.norrish%40anu.edu.au%7C26fb8f53e88547f71fcb08d9d8e7092e%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637779763804684071%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000sdata=iIPqCbidb5lDxeTnWT8Yf5Rzmym1c3JOfm3J3ANhKa4%3Dreserved=0

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.