Use WebWorkers and add a cache

mit-plv · Nov 19, 2023 · e417a02 · e417a02
1 parent 0f1088d
commit e417a02
Show file tree

Hide file tree

Showing 3 changed files with 83 additions and 27 deletions.
diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html
@@ -51,6 +51,7 @@
             <button type="button" id="cancelButton" disabled>Cancel</button>
             <span id="status" class="status-span hidden"></span>
             <a id="permalink" class="permalink-span hidden" href="#">Pseudopermalink</a>
+            <button type="button" id="clearCacheButton">Clear Cache</button>
         </div>
     </form>
     <div id="error" class="error hidden"></div>
@@ -64,7 +65,6 @@
         <button class="copy-button" data-target="stderr">Copy</button>
       </div>
     </div>
-    <script src="fiat_crypto.js"></script>
     <script src="main.js"></script>
     <script src="copy-button.js"></script>
 </body>

diff --git a/fiat-html/fiat_crypto_worker.js b/fiat-html/fiat_crypto_worker.js
@@ -0,0 +1,5 @@
+self.importScripts("fiat_crypto.js");
+self.onmessage = function(e) {
+    const result = synthesize(e.data);
+    postMessage(result);
+};
diff --git a/fiat-html/main.js b/fiat-html/main.js
@@ -1,4 +1,5 @@
 // Written with help from https://chat.openai.com/share/74d5901c-9005-4560-8307-582ff54e403e
+const SYNTHESIS_CACHE_VERSION = 1;
 document.addEventListener('DOMContentLoaded', function() {
     const errorDiv = document.getElementById('error');
     const outputDiv = document.getElementById('output');
@@ -10,6 +11,7 @@ document.addEventListener('DOMContentLoaded', function() {
     const inputArgs = document.getElementById('inputArgs');
     const synthesizeButton = document.getElementById('synthesizeButton');
     const cancelButton = document.getElementById('cancelButton');
+    const clearCacheButton = document.getElementById('clearCacheButton');
     const permalink = document.getElementById('permalink');
     const statusSpan = document.getElementById('status');
     const isSafari = /^((?!chrome|android).)*safari/i.test(navigator.userAgent);
@@ -135,7 +137,7 @@ document.addEventListener('DOMContentLoaded', function() {
         }
     }
 
-    function handleSynthesisResult(result) {
+    function handleSynthesisResultData(result) {
         const success = result[0];
         const exceptionText = result[1];
         const stdout = result[2];
@@ -168,40 +170,82 @@ document.addEventListener('DOMContentLoaded', function() {
         updateStatus(""); // Clear status
     }
 
+    function handleSynthesisResult(result, cached) {
+        const cachedString = cached ? ` (cached on ${result.timestamp})` : '';
+        if (result.success) {
+            clearOutput();
+            updateStatus(`Synthesis${cachedString} completed in ${result.time} seconds`);
+            handleSynthesisResultData(result.result);
+        } else {
+            handleException(result.result);
+            updateStatus(`Synthesis${cachedString} failed in ${result.time} seconds`);
+        }
+    }
 
+    let synthesisWorker;
+
+    function setupSynthesisWorker() {
+        synthesisWorker = new Worker("fiat_crypto_worker.js");
+
+        synthesisWorker.onmessage = function(e) {
+            console.log(`Early synthesis result: ${e.data}`);
+        };
+
+        synthesisWorker.onerror = function(err) {
+            handleException(err);
+        };
+    }
+
+    function cancelSynthesisWorker() {
+        if (synthesisWorker) {
+            synthesisWorker.terminate();
+            console.log("Synthesis worker terminated.");
+        }
+        setupSynthesisWorker(); // Re-setup the worker for future use
+    }
 
-    var curSynthesisPromise;
     function handleSynthesis(args) {
         const startTime = performance.now();
+        const cacheKey = 'synthesize_' + JSON.stringify(args);
+        const cached = localStorage.getItem(cacheKey);
         console.log({'synthesize args': args});
         updateStatus("Synthesizing...");
         updatePermalink(args);
-        const synthesisPromise = new Promise((resolve, reject) => {
-            try {
-                resolve(synthesize(args))
-            } catch (error) {
-                reject(error);
+
+        if (cached) {
+            const cachedData = JSON.parse(cached);
+            if (cachedData.version === SYNTHESIS_CACHE_VERSION) {
+                handleSynthesisResult(cachedData, true);
+                return;
+            } else {
+                console.log(`cache miss: version ${cachedData.version}, expected ${SYNTHESIS_CACHE_VERSION}`)
             }
-        });
-        curSynthesisPromise = synthesisPromise;
-        synthesisPromise
-            .then((value) => {
-                if (curSynthesisPromise === synthesisPromise) {
-                    const endTime = performance.now();
-                    clearOutput();
-                    updateStatus(`Synthesis completed in ${(endTime - startTime) / 1000} seconds`);
-                    handleSynthesisResult(value);
-                } else {
-                    console.log(`Synthesis of ${args} completed after being canceled: ${value}`);
-                }
-            })
-            .catch((err) => {
-                if (curSynthesisPromise === synthesisPromise) {
-                    handleException(err);
-                } else {
-                    console.log(`Synthesis of ${args} errored after being canceled: ${err}`);
+        }
+
+        const recieveMessage = function (success) {
+            return function(e) {
+                const endTime = performance.now();
+                const timeTaken = (endTime - startTime) / 1000;
+                const now = new Date();
+                const resultData = {
+                    result: e.data,
+                    time: timeTaken,
+                    success: success,
+                    timestamp: now.toISOString(),
+                    version: SYNTHESIS_CACHE_VERSION
+                };
+                try {
+                    localStorage.setItem(cacheKey, JSON.stringify(resultData));
+                } catch (e) {
+                    console.error(`Failed: localStorage.setItem(${JSON.stringify(cacheKey)}, ${JSON.stringify(JSON.stringify(resultData))})`);
                 }
-            });
+                handleSynthesisResult(resultData, false);
+            };
+        };
+
+        synthesisWorker.postMessage(args);
+        synthesisWorker.onmessage = recieveMessage(true);
+        synthesisWorker.onerror = recieveMessage(false);
     }
 
     function parseAndRun(argv) {
@@ -214,6 +258,8 @@ document.addEventListener('DOMContentLoaded', function() {
         }
     }
 
+    setupSynthesisWorker();
+
     const queryParams = new URLSearchParams(window.location.search);
     const argv = queryParams.get('argv');
     const interactive = queryParams.get('interactive');
@@ -267,5 +313,10 @@ document.addEventListener('DOMContentLoaded', function() {
         synthesizeButton.disabled = false;
         cancelButton.disabled = true;
         updateStatus("");
+        cancelSynthesisWorker();
+    });
+
+    clearCacheButton.addEventListener('click', function() {
+        localStorage.clear();
     });
 });