Insights into Biological Synthesis Techniques and Related Work
Explore the biological synthesis project by Sumay and Sumit Gulwani at MSR Redmond. The project delves into template-based approaches and safety considerations in artifact synthesis. The outline covers inductive synthesis, challenges, and successes in achieving synthesis goals. Discover unique naming strategies and the significance of related works in this domain.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Biological Synthesis Sumit Gulwani MSR Redmond April 2013
Outline Synthesis Techniques: Template-based & Inductive Safety & Liveness properties of synthesized artifact Results Grant ExCAPE (a multi-million dollar NSF grant on Synthesis) Conclusion 1
Biological Synthesis Project Sumay Sumit Gulwani MSR Redmond Joint work with Monika Gulwani April 2013
Template based approach to a WiSE name Monika s constraints: neither popular on Bing (Sorry uncle Ben, uncle Tom) nor Big Musical and easy to Pronounce elegant Semantics Sumit s approach: Template based strategy: C V C V C (where C=consonant, V=vowel) Pruning strategy: Pick a CV pair from each creator, including initials. Solution space: MoSu_, MoSi_, MiSu_, MiSi_, MaSu_, MaSi_ SuMo_, SuMi_, SuMa_, SiMo_, SiMi_, SiMa_, Potential solutions: MaSum => Too gentle SuMit => Need a different name than creator SuMan => A bit feminine SuMay=> meaning wise in Hindi. That s how dad gets a Bonus for having mom s initial in his name at right place! 3
Related Work Before we jump-start the project, due diligence to related work is met: Project Aashika by Kavita & Madan Musuvathi Project Anna Rose by Emilie & Todd Mytkowicz 4
Inductive Synthesis Sumay was 12 days past the deadline. Planned inductive procedure was used to get him out. Good news: 1 unit of induction was good enough. Monika wanted to compete with my other distraction (FlashFill) that is also known to work well with minimum inductive units. But Monika wanted to more than even out: Sumay was born on O1/O2/O3 @ O4 hrs O5 min (where Oi = odd #) 5
Sumay_&_Mom.Sleep() Well-deserved rest in hospital. Dad.Watch_Sumay_&_Mom_fromHisCot(); Nikolaj: They won t be quiet for long! 6
Safety Property: Event DiaperChange handled properly Property: Handler of event DiaperChange should not be pre- empted by another occurrence of that event. @Clousot: Warning: Property not satisfied . @Monika: It is a false positive. Found a counterexample next day: Event DiaperChange occurred twice before the handler could finish. @Francesco: Invoke garbage collector (GC) immediately when DiaperChange occurs to mask off other invocations. Problem: GC is too small & sometimes gets pre-empted. 7
Safety Property: Event DiaperChange handled properly Property: Handler of event DiaperChange should not be pre- empted by another occurrence of that event. @Clousot: Warning: Property not satisfied . @Monika: It is a false positive. Found a counterexample next day: Event DiaperChange occurred twice before the handler could finish. @Francesco: Invoke garbage collector (GC) immediately when DiaperChange occurs to mask off other invocations. Problem: GC is too small & sometimes gets pre-empted. Solution: @Babyrus: Run handler within DiaperChangePad lock. @Target: Use wipe warmer to make Environment less adversarial. 8
Liveness Property: Crying stops eventually If (DiaperChangeEvent) { ... } Else { If (RecentlyFed) { Try { Burping() }; Catch (Timeout Exception) { DadSurfaceMagic(); } } Else { Try { Feeding() }; Catch (NotInterested Exception) { DadSurfaceMagic(); } } } 9
Procedure DadSurfaceMagic() // Summary: Sumay enjoys tummy time on Dad s chest. Step 1: Hold Sumay. Assert(Sumay stops crying but is breathing fast); Step 2: Sit down on couch. Open the recliner (to 22 degrees) and lie down. Assert(Sumay is calm & his breathing speed starts matching Dad s relaxed breathing speed & soon goes off to sleep); 10
Results Who does Sumay look like? Sumay looks like his dad: 70% Incomparable element: 15% Monika looks like Sumay: 15% How-am-I-doing test on 3rd day @ hospital: Breast-feeding well Hair denser than his dad As pink as he can be Excels in cuteness test Lovely flowers courtesy RiSE 11
Grand ExCAPE to Cherry Blossom For those evil eyed folks, who were aghast at seeing me so very refreshed 2 weeks later in office : This was the result of Dad_&_Father-in-law.Run() triggered by simultaneous happening of 3 events on 12th day: Mom.Post-partum_Lows Sumay.Fussiness Mother-in-law.Unnamed 12
Proud Academic Genealogy Mentor Sumit Gulwani Signed him up for experiment in Education Grand-mentor George Necula Sent well-thought gifts including Baby Einstein music CD (known to improve IQ). Great grand-mentor Peter Lee Managed to keep track of his growing genealogy: Wow, congratulations! Sue and I are very happy for you and your family. 13
Some cute quotes Nikolaj Bjorner: Enjoy: Baby Sleep Guide: Sleep Solutions for You & Your Baby . I hope your constraint system is going to be feasible and that there not only exists a non-empty set of solutions, but that they can also be found within reasonable time. Shobana Balakrishnan: Sumay the wise one! Wonder how soon before he will start disproving some of your theories! Aditya Nori: hello world to Sumay Rico Malvar: Sumay looks very handsome - and happy Dad (to Mom): Look, I taught Sumay the photogenic lesson. Mom: But, I saw him smiling with open eyes at birth. Learns to sleep Learns to smile in sleep Learns to smile with open eyes At birth
