BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:STANDARD DTSTART:20141102T020000 RDATE:20141102T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20141103T220133Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141111T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141111T110000 DTSTAMP;VALUE=DATE-TIME:20141103T220133Z LAST-MODIFIED;VALUE=DATE-TIME:20141103T220133Z UID:http://calagator.org/events/1250467279 DESCRIPTION:abstract: \;\nRead-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer lock ing (among other things) that was added to the Linux kernel in 2002. A s imilar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel i n 1993\, and antecedents go back to at least 1980. Although a fully func tional textbook implementation of RCU comprises only about 20 lines of c ode\, the Linux-kernel implementation comprises more than 15\,000 lines of code due to harsh requirements involving performance\, scalability\, energy efficiency\, real-time response\, memory footprint\, module unloa ding\, hotplugging of CPUs\, and software-engineering considerations. 3\;\n \;\nTherefore\, a key Linux-kernel RCU challenge is validation and verification. To this end\, more than 2500 lines of the current Linu x-kernel implementation do torture testing. However\, there are now more than one billion devices running Linux\, so that an RCU bug that manife sted on average once every million years of machine time would manifest about three times every day across the installed base. Furthermore\, the combination of Internet of Things and Josh Triplett’s Linux Kernel Tini fication project is likely to significantly increase the number of runni ng instances. \;\n \;\nI write and run rcutorture tests myself\, a nd I like to think that my 20 years of parallel-code testing experience allows me to meet this validation challenge\, but a simple analysis sugg ests a gap of several orders of magnitude. Additional validation and ver ification techniques are thus called for. This talk gives a brief overvi ew of RCU and describes my adventures evaluating various verification te chniques. \;\n \;\nbio: \;\nPaul E. McKenney has been coding fo r almost four decades\, more than half of that on parallel hardware\, wh ere his work has earned him a reputation among some as a flaming heretic . Over the past decade\, Paul has been an IBM Distinguished Engineer at the IBM Linux Technology Center. Paul maintains the RCU implementation w ithin the Linux kernel\, where the variety of workloads present highly e ntertaining performance\, scalability\, real-time response\, and energy- efficiency challenges. Prior to that\, he worked on the DYNIX/ptx kernel at Sequent\, and prior to that on packet-radio and Internet protocols ( but long before it was polite to mention Internet at cocktail parties)\, system administration\, business applications\, and real-time systems. He has a BS in Computer Science and another in Mechanical Engineering al ong with an MS in Computer Science\, all from Oregon State University. H e also has a Ph.D. in Computer Science and Engineering from OGI/OHSU. He has more than 100 publications and more than 50 patents. His hobbies in clude what passes for running at his age along with the usual house-wife -and-kids habit.\n\nTags: Galois tech talk\, linux\, read-copy update\, verification\, validation\n\nImported from: http://calagator.org/events/ 1250467279 URL:http://galois.com/blog/2014/11/tech-talk-read-copy-update-rcu-validat ion-verification-linux/ SUMMARY:Galois tech talk: Read-copy update (RCU) validation and verificat ion for Linux LOCATION:Galois Inc: 421 Sw 6th Ave Ste 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR