Finish the pipelining chapter

1 files changed, 19 insertions, 0 deletions

diff --git a/lsr_refs.bib b/lsr_refs.bib
index abfd180..a107605 100644
--- a/lsr_refs.bib
+++ b/lsr_refs.bib
@@ -305,6 +305,25 @@
 	year = {2011}
 }
 
+@article{courant21_verif_code_gener_polyh_model,
+	author = {Courant, Nathanaël and Leroy, Xavier},
+	title = {Verified Code Generation for the Polyhedral Model},
+	year = {2021},
+	issue_date = {January 2021},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	volume = {5},
+	number = {POPL},
+	url = {https://doi.org/10.1145/3434321},
+	doi = {10.1145/3434321},
+	abstract = {The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary and difficult to regenerate sequential or parallel loop nests before continuing compilation. This paper reports on the formalization and proof of semantic preservation of such a code generator that produces sequential code from a polyhedral representation. The formalization and proofs are mechanized using the Coq proof assistant.},
+	journal = {Proc. ACM Program. Lang.},
+	month = {jan},
+	articleno = {40},
+	numpages = {24},
+	keywords = {Compiler verification, Polyhedral code generation, Polyhedral model}
+}
+
 @inbook{coussy08_gaut,
 	abstract = {This chapter presents GAUT, an academic and open-source high-level synthesis tool dedicated to digital signal processing applications. Starting from an algorithmic bit-accurate specification written in C/C++, GAUT extracts the potential parallelism before processing the allocation, the scheduling and the binding tasks. Mandatory synthesis constraints are the throughput and the clock period while the memory mapping and the I/O timing diagram are optional. GAUT next generates a potentially pipelined architecture composed of a processing unit, a memory unit and a communication with a GALS/LIS interface.},
 	author = {Coussy, Philippe and Chavet, Cyrille and Bomel, Pierre and Heller, Dominique and Senn, Eric and Martin, Eric},