ชีวิตป.เอกเทอมสาม

Posted on March 30, 2015

อัพเดทข่าวคราวสำหรับครอบครัวและเพื่อนที่อยากรู้ความเป็นไป
สำหรับความเป็นไปของเทอม 2 ให้เข้าไปอ่านที่นี่
(https://amchiclet.wordpress.com/2014/08/20/%E0%B8%8A%E0%B8%B5%E0%B8%A7%E0%B8%B4%E0%B8%95%E0%B8%9B-%E0%B9%80%E0%B8%AD%E0%B8%81%E0%B9%80%E0%B8%97%E0%B8%AD%E0%B8%A1%E0%B8%AA%E0%B8%AD%E0%B8%87/)

อันนี้เขียนย้อนหลัง เกี่ยวกับหน้าร้อนปีที่แล้ว (พฤษภาคมปีที่แล้ว)

ถือว่าเป็นซัมเมอร์แรกตั้งแต่มาอยู่ที่นี่

หลังจากได้เดวิดเป็นอาจารย์ที่ปรึกษา
เดวิดขอร้องให้เราใช้หน้าร้อนนี้ทำวัจัยที่มหาลัย

ก็จ๋อยๆไปนิดเพราะอดสมัครฝึกงานแถวๆ ซิลิคอน ว่าเล่ย์ ที่เค้าล่ำลือกัน
แต่โดยสรุปแล้วมีเรื่องสนุกๆเกิดขึ้นเยอะเหมือนกัน

การเรียน

เทอมนี้ไม่มีเรียนเฟ่ย

การวิจัย

เดวิดอธิบายโปรเจควิจัยให้เราฟัง

เราก็พอได้ไอเดีย แต่ยังเลือนลางอยู่

เดวิดก็เลยเริ่มจัด textbook มาให้หนึ่งเล่ม หนาประมาณ 600 หน้าถ้าจำไม่ผิด
แล้วเดวิดก็บอกกับเราว่า “อ่านทั้งเล่มเถอะนะคนดี”

ก็เป็นหนังสือเกี่ยวกับว่าพวก compiler มันทำอะไรกับ code ของเราให้เร็วขึ้นบ้าง
เพราะว่าโปรเจคของเราจะต้องเอาไปใช้

จากนั้นไม่นานเดวิดก็มอบหมายภารกิจอีกหนึ่งชิ้นให้ ก็คือ
ให้ไปเยี่ยม อาจารย์อีกคนนึงซึ่งชื่อว่า เจเรมี่
แล้วไปเรียนรู้กับเค้าหนึ่งสัปดาห์ว่าโปรเจคต้องทำอะไรบ้าง

ก็จัดไป

บินไปลงที่เมืองที่ชื่อว่า philadelphia (อ่านว่า ฟิน ลา เดว เฟีย)
ซึ่งเป็นเมืองที่คนชอบเยอะมาก ยกเว้นเรา เพราะรู้สึกว่าเมืองมันน่ากลัวๆยังไงก็ไม่รู้

ไปถึงแล้วก็นั่งรถไฟไปหา เจเรมี่ ที่มหาลัยของเค้า

พอเจอเจเรมี่ เค้าก็พาเราเข้าไปในออฟฟิส

เจเรมี่ก็ให้คำสั่งแรกคือ จงโหลดโปรแกรมที่ชื่อว่า isabelle (อ่านว่า อิ ซา เบว) แล้วเปิดมันขึ้นมา
ระหว่างโหลดอยู่ เจเรมี่ ก็ส่ง pdf ไฟล์มาอันนึง
แล้วบอกว่า จากนี้ไปเราจะอ้างอิงหนังสือนี้เป็นจุดเริ่มต้นของงานวิจัยเรา

ทุกๆอย่างก็เริ่มเป็นชิ้นเป็นอัน

สรุปว่าโปรเจคของเราก็คือ การหาวิธีทำให้ compiler พันธุ์ดุ ผลิต code ที่เร็วขึ้น

ขยายความ compiler พันธุ์ดุ

ปกติ compiler ดีๆปัจจุบัน มันทำหน้าที่หลักๆก็คือ
1. หา bug ใน code เท่าที่หาได้
2. ทำให้ code เร็วขึ้น
3. แปลง code จากภาษาที่มนุษย์เข้าใจ ให้เป็นภาษาที่เคร่ื่องคอมพิวเตอร์เข้าใจ

ทีนี้ตัว compiler เองมันก็มี bug เหมือนกัน
แล้วในกรณีที่แย่ที่สุดคือ compiler แปลง code ผิด

ผลลัพธ์คือ code ที่ผลิตออกมา อาจจะมีช่องโหว่ ให้พวก hacker จู่โจมได้
เช่น เครื่องบินสำรวจอาจจะโดนข้าศึก hack แล้วยึดไปได้
(เอาลิงค์ไปดูมันส์ๆ http://www.cbsnews.com/videos/creating-drones-that-cant-be-hacked/)

มันก็เลยมีการวิจัยเกี่ยวกับ compiler พันธุ์ดุออกมา (ชื่อวิชาการว่า verified compiler)
ซึ่งเป็น compiler ซึ่งได้พิสูจน์ทางคณิตศาสตร์แล้วว่า ไม่ได้เพิ่มอะไรผิดๆเข้าไปใน code

แล้วการพิสูจน์ทางคณิตศาสตร์เนี่ย
ถ้าเขียนบนกระดาษ มันอาจจะพิสูจน์ถูก พิสูจน์ผิดได้
คนเราก็มักจะทำความผิดพลาดเสมอใช่มะ
ก็เลยมีโปรแกรมสำหรับให้คอมพิวเตอร์ช่วยตรวจข้อพิสูจน์เหล่านั้น
ซึ่งหนึ่งตัวอย่างของ โปรแกรมช่วยเขียนและตรวจข้อพิสูจน์ก็คือ isabelle นี่เอง

ทุกอย่างฟังดูดี
แต่ปัญหาของ compiler พันธุ์ดุ ก็คือ มันไม่เก่งเรื่องทำให้ code เร็วขึ้น

โปรเจคของเราคือ ดูซิว่ามีวิธีไหนบ้างที่เราจะช่วย compiler พันธุ์ดุ พวกนี้ทำให้ code เร็วขึ้นได้ยังไงบ้าง
แล้วก็ต้องอย่าลืม พิสูจน์ทางคณิตศาสตร์ด้วยว่า compiler ไม่มี bug

หนึ่งสัปดาห์ที่อยู่กับเจเรมี่ส่วนใหญ่ก็ฝึกการใช้ isabelle
กับการพิสูจน์พวกความถูกต้องของการ compile ง่ายๆ สำหรับภาษาโปรแกรมเล็กๆ

สรุป ซัมเมอร์นี้ ไม่เสียเปล่า
ได้เปิดหูเปิดตา กับอะไรที่เรารู้สึกว่า เจ๋งเป้ง
แล้วก็ได้ทำความคุ้นเคยกับการพิสูจน์แบบมีคอมพิวเตอร์ช่วย