regenerate after: Update 2024fa.md

lsd-ucsc · Nov 21, 2024 · eb3e6ad · eb3e6ad
1 parent 35c9461
commit eb3e6ad
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 9 deletions.
diff --git a/index.xml b/index.xml
@@ -84,7 +84,7 @@
 &lt;tr&gt;
 &lt;td&gt;&lt;a href=&#34;#nov-22&#34;&gt;Nov 22&lt;/a&gt;&lt;/td&gt;
 &lt;td&gt;Haining Tong&lt;/td&gt;
-&lt;td&gt;&lt;em&gt;TBD&lt;/em&gt;&lt;/td&gt;
+&lt;td&gt;Towards Unified Analysis of GPU Consistency&lt;/td&gt;
 &lt;/tr&gt;
 
 &lt;tr&gt;
@@ -187,11 +187,11 @@
 
 &lt;p&gt;&lt;strong&gt;Speaker:&lt;/strong&gt; Haining Tong&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; Towards Unified Analysis of GPU Consistency&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; After more than 30 years of research, there is a solid understanding of the consistency guarantees given by CPU systems. Unfortunately, the same is not yet true for GPUs. The growing popularity of general purpose GPU programming has been a call for action which industry players like NVIDIA and Khronos have answered by formalizing their PTX and Vulkan consistency models. These models give precise answers to questions about program&amp;rsquo;s correctness. However, interpreting them still requires a level of expertise that escapes most developers, and the current tool support is insufficient. To remedy this, we translated and integrated the PTX and Vulkan models into the Dartagnan verification tool. This makes Dartagnan the first analysis tool for multiple GPU consistency models that can analyze real GPU code. During the validation of the translated models, we discovered two bugs in the original PTX and Vulkan consistency models.&lt;/p&gt;
 
-&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; &lt;em&gt;TBD&lt;/em&gt;&lt;/p&gt;
+&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; Haining is a Computer Science Ph.D. student advised by Keijo Heljanko at the University of Helsinki. His work focuses on using formal verification techniques to analyze GPU memory consistency models.&lt;/p&gt;
 
 &lt;h2 id=&#34;dec-6&#34;&gt;Dec 6&lt;/h2&gt;
 

diff --git a/lsd-seminar/2024fa/index.html b/lsd-seminar/2024fa/index.html
@@ -265,7 +265,7 @@ <h1 itemprop="name">Languages, Systems, and Data Seminar (Fall 2024)</h1>
 <tr>
 <td><a href="#nov-22">Nov 22</a></td>
 <td>Haining Tong</td>
-<td><em>TBD</em></td>
+<td>Towards Unified Analysis of GPU Consistency</td>
 </tr>
 
 <tr>
@@ -368,11 +368,11 @@ <h2 id="nov-22">Nov 22</h2>
 
 <p><strong>Speaker:</strong> Haining Tong</p>
 
-<p><strong>Title:</strong> <em>TBD</em></p>
+<p><strong>Title:</strong> Towards Unified Analysis of GPU Consistency</p>
 
-<p><strong>Abstract:</strong> <em>TBD</em></p>
+<p><strong>Abstract:</strong> After more than 30 years of research, there is a solid understanding of the consistency guarantees given by CPU systems. Unfortunately, the same is not yet true for GPUs. The growing popularity of general purpose GPU programming has been a call for action which industry players like NVIDIA and Khronos have answered by formalizing their PTX and Vulkan consistency models. These models give precise answers to questions about program&rsquo;s correctness. However, interpreting them still requires a level of expertise that escapes most developers, and the current tool support is insufficient. To remedy this, we translated and integrated the PTX and Vulkan models into the Dartagnan verification tool. This makes Dartagnan the first analysis tool for multiple GPU consistency models that can analyze real GPU code. During the validation of the translated models, we discovered two bugs in the original PTX and Vulkan consistency models.</p>
 
-<p><strong>Bio:</strong> <em>TBD</em></p>
+<p><strong>Bio:</strong> Haining is a Computer Science Ph.D. student advised by Keijo Heljanko at the University of Helsinki. His work focuses on using formal verification techniques to analyze GPU memory consistency models.</p>
 
 <h2 id="dec-6">Dec 6</h2>
 

diff --git a/themes/academic b/themes/academic