Răsfoiți Sursa

more about microsoft x64

Jeremy Siek 4 ani în urmă
părinte
comite
d688d7b40e
2 a modificat fișierele cu 75 adăugiri și 15 ștergeri
  1. 56 1
      all.bib
  2. 19 14
      book.tex

+ 56 - 1
all.bib

@@ -2,13 +2,68 @@
 %% http://bibdesk.sourceforge.net/
 
 
-%% Created for Jeremy Siek at 2020-10-13 13:16:37 -0400 
+%% Created for Jeremy Siek at 2020-11-04 10:45:27 -0500 
 
 
 %% Saved with string encoding Unicode (UTF-8) 
 
 
 
+@misc{Microsoft:2018ac,
+	Author = {Microsoft},
+	Date-Added = {2020-11-04 09:44:59 -0500},
+	Date-Modified = {2020-11-04 10:45:03 -0500},
+	Howpublished = {\url{https://docs.microsoft.com/en-us/cpp/build/prolog-and-epilog}},
+	Month = {December},
+	Title = {x64 prolog and epilog},
+	Year = {2018}}
+
+@misc{Microsoft:2018ab,
+	Author = {Microsoft},
+	Date-Added = {2020-11-04 09:40:30 -0500},
+	Date-Modified = {2020-11-04 10:45:16 -0500},
+	Howpublished = {\url{https://docs.microsoft.com/en-us/cpp/build/stack-usage}},
+	Month = {December},
+	Title = {x64 stack usage},
+	Year = {2018}}
+
+@misc{Microsoft:2020aa,
+	Author = {Microsoft},
+	Date-Added = {2020-11-04 09:37:09 -0500},
+	Date-Modified = {2020-11-04 10:45:27 -0500},
+	Howpublished = {\url{https://docs.microsoft.com/en-us/cpp/build/x64-calling-convention}},
+	Month = {July},
+	Title = {x64 calling convention},
+	Year = {2020}}
+
+@misc{Microsoft:2018aa,
+	Author = {Microsoft},
+	Date-Added = {2020-11-04 09:34:51 -0500},
+	Date-Modified = {2020-11-04 10:44:30 -0500},
+	Howpublished = {\url{https://docs.microsoft.com/en-us/windows-hardware/drivers/debugger/x64-architecture}},
+	Month = {March},
+	Title = {x64 Architecture},
+	Year = {2018}}
+
+@misc{Williams:2020aa,
+	Author = {Stelios Tsampas 􏰔and Christian Williams and Dominique Devriese and Frank Piessens1},
+	Date-Added = {2020-10-20 09:44:37 -0400},
+	Date-Modified = {2020-10-20 09:48:15 -0400},
+	Howpublished = {arXiv:2010.07899 [cs.LO]},
+	Month = {October},
+	Title = {Abstract Congruence Criteria for Weak Bisimilarity},
+	Year = {2020},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXjIwMTAuMDc4OTkucGRmTxEBSAAAAAABSAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////DjIwMTAuMDc4OTkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAKi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjoyMDEwLjA3ODk5LnBkZgAOAB4ADgAyADAAMQAwAC4AMAA3ADgAOQA5AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAoVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi8yMDEwLjA3ODk5LnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJAAzAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAX8=}}
+
+@inproceedings{Nipkow:2020aa,
+	Author = {Tobias Nipkow and Manuel Eberl and Maximilian P.L. Haslbeck},
+	Booktitle = {Automated Technology for Verification and Analysis},
+	Date-Added = {2020-10-19 09:30:58 -0400},
+	Date-Modified = {2020-10-19 09:32:22 -0400},
+	Title = {Verified Textbook Algorithms: A Biased Survey},
+	Year = {2020},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAxTmlwa293MjAyMF9DaGFwdGVyX1ZlcmlmaWVkVGV4dGJvb2tBbGdvcml0aG1zLnBkZk8RAdYAAAAAAdYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////x9OaXBrb3cyMDIwX0NoYXB0ZXIjRkZGRkZGRkYucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAFBERiAAAAAAAAEAAgAACiBjdQAAAAAAAAAAAAAAAAADYmliAAACAE0vOlVzZXJzOmpzaWVrOkRvY3VtZW50czpiaWI6Tmlwa293MjAyMF9DaGFwdGVyX1ZlcmlmaWVkVGV4dGJvb2tBbGdvcml0aG1zLnBkZgAADgBkADEATgBpAHAAawBvAHcAMgAwADIAMABfAEMAaABhAHAAdABlAHIAXwBWAGUAcgBpAGYAaQBlAGQAVABlAHgAdABiAG8AbwBrAEEAbABnAG8AcgBpAHQAaABtAHMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEtVc2Vycy9qc2llay9Eb2N1bWVudHMvYmliL05pcGtvdzIwMjBfQ2hhcHRlcl9WZXJpZmllZFRleHRib29rQWxnb3JpdGhtcy5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFgAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACMg==}}
+
 @article{Collins:1960aa,
 	Abstract = {An important property of the Newell Shaw-Simon scheme for computer storage of lists is that data having multiple occurrences need not be stored at more than one place in the computer. That is, lists may be ``overlapped.'' Unfortunately, overlapping poses a problem for subsequent erasure. Given a list that is no longer needed, it is desired to erase just those parts that do not overlap other lists. In LISP, McCarthy employs an elegant but inefficient solution to the problem. The present paper describes a general method which enables efficient erasure. The method employs interspersed reference counts to describe the extent of the overlapping.},
 	Address = {New York, NY, USA},

+ 19 - 14
book.tex

@@ -253,23 +253,28 @@ The book uses the Racket language both for the implementation of the
 compiler and for the language that is compiled, so a student should be
 proficient with Racket (or Scheme) prior to reading this book. There
 are many excellent resources for learning Scheme and
-Racket~\citep{Dybvig:1987aa,Abelson:1996uq,Friedman:1996aa,Felleisen:2001aa,Felleisen:2013aa,Flatt:2014aa}. It
-is helpful but not necessary for the student to have prior exposure to
-the x86 (or x86-64) assembly language~\citep{Intel:2015aa}, as one
-might obtain from a computer systems
-course~\citep{Bryant:2005aa,Bryant:2010aa}. This book introduces the
+Racket~\citep{Dybvig:1987aa,Abelson:1996uq,Friedman:1996aa,Felleisen:2001aa,Felleisen:2013aa,Flatt:2014aa}.
+
+It is helpful but not necessary for the student to have prior exposure
+to the x86 assembly language~\citep{Intel:2015aa}, as one might obtain
+from a computer systems
+course~\citep{Bryant:2010aa}. This book introduces the
 parts of x86-64 assembly language that are needed.
 %
-We follow the System V calling conventions~\citep{Matz:2013aa}, which
-means that the assembly code that we generate will work properly with
-our runtime system (written in C) when it is compiled using the GNU C
-compiler (\code{gcc}) on Linux or MacOS. (Minor adjustments are needed
-for MacOS, which we note as they arise.)
+We follow the System V calling
+conventions~\citep{Bryant:2005aa,Matz:2013aa}, which means that the
+assembly code that we generate will work properly with our runtime
+system (written in C) when it is compiled using the GNU C compiler
+(\code{gcc}) on the Linux and MacOS operating systems. (Minor
+adjustments are needed for MacOS which we note as they arise.)
 %
-The Microsoft Windows operating system uses a different calling
-convention~\citep{Microsoft:2018aa}, which is followed by the GNU C
-compiler when running on Windows. So the assembly code that we
-generate will \emph{not} work on Windows.
+When running on the Microsoft Windows operating system, the GNU C
+compiler follows the Microsoft x64 calling
+convention~\citep{Microsoft:2018aa,Microsoft:2020aa}. So the assembly
+code that we generate will \emph{not} work properly with our runtime
+system on Windows. We include challenge exercises that give some hints
+regarding how to adapt the code generation to the Windows x64
+conventions.
 
 
 %\section*{Structure of book}