008240612s2023      us  |||||||||||||||c||eng  d
■001000016933332
■00520240214101233
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798379905941
■035    ▼a(MiAaPQ)AAI30527663
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aVan  Geffen,  Jacob.
■24510▼aProgram  Synthesis  for  Systems  Developers▼h[electronic  resource]
■260    ▼a[S.l.]:▼bUniversity  of  Washington.  ▼c2023
■260  1▼aAnn  Arbor  :▼bProQuest  Dissertations  &  Theses,  ▼c2023
■300    ▼a1  online  resource(101  p.)
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-01,  Section:  B.
■500    ▼aAdvisor:  Torlak,  Emina.
■5021  ▼aThesis  (Ph.D.)--University  of  Washington,  2023.
■506    ▼aThis  item  must  not  be  sold  to  any  third  party  vendors.
■520    ▼aImplementing  and  verifying  the  correctness  of  systems  software  poses  a  difficult  challenge  for  developers.  Systems  software  operates  across  multiple  levels  of  abstraction,  requiring  developers  to  reason  about  the  interactions  between  these  abstraction  layers.  At  the  same  time,  ensuring  correctness  of  these  systems  is  now  more  important  than  ever.  Linux  kernel  vulnerabilities  can  allow  malicious  users  to  gain  root  access  in  critical  systems,  and  incorrectly  implemented  cloud  storage  systems  can  harm  data  availability  for  millions  of  users.This  dissertation  presents  two  novel  program  synthesis  tools  that  automate  the  implementation  and  verification  of  two  classes  of  systems:  in-kernel  just-in-time  (JIT)  compilers  and  crash  consistent  storage  systems.  The  first  of  these  tools,  JITSYNTH,  allows  kernel  developers  to  automatically  generate  correct  in-kernel  JIT  compilers  by  giving  a  specification  of  the  source  and  target  language.  These  JITs  translate  user-submitted  programs  to  lower-level  assembly  code  for  kernel  execution.  Manually  implementing  (and  proving  correctness  of)  these  JITs  poses  a  difficult  challenge  for  developers  due  to  subtle  differences  in  the  semantics  of  the  source  and  target  languages.  By  synthesizing  JITs  automatically,  JITSYNTH  allows  developers  to  avoid  kernel-breaking  bugs  without  the  massive  effort  of  implementing  and  verifying  a  new  compiler  for  each  target  architecture.  The  second  tool  presented,  DEPSYNTH,  enables  storage  system  developers  to  automatically  add  crash  consistency  mechanisms  to  their  systems.  Designing  crash  consistent  systems  is  difficult  for  developers  because  it  requires  reasoning  about  complex  constraints  on  the  orderings  of  storage  system  writes.  DEPSYNTH  allows  developers  to  reap  the  data  availability  and  resiliency  benefits  of  crash  consistency  without  the  overhead  of  manually  reasoning  about  these  orderings.  Together,  these  tools  demonstrate  the  effectiveness  of  program  synthesis  for  developing  systems  software.
■590    ▼aSchool  code:  0250.
■650  4▼aComputer  science.
■650  4▼aComputer  engineering.
■653    ▼aCompilers
■653    ▼aProgram  synthesis
■653    ▼aStorage  systems
■653    ▼aMalicious  users
■653    ▼aDesigning  crash
■690    ▼a0984
■690    ▼a0464
■71020▼aUniversity  of  Washington▼bComputer  Science  and  Engineering.
■7730  ▼tDissertations  Abstracts  International▼g85-01B.
■773    ▼tDissertation  Abstract  International
■790    ▼a0250
■791    ▼aPh.D.
■792    ▼a2023
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16933332▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.
■980    ▼a202402▼f2024