pgo

PGO

PGO เป็นแหล่งที่มาของคอมไพเลอร์แหล่งที่มาซึ่งแปลข้อกำหนดของโมดูลาร์บวก (ซึ่งใช้ superset ของ pluscal) เป็นโปรแกรม GO

นอกเหนือจากคอมไพเลอร์ PGO แล้วต้นไม้ต้นฉบับนี้ยังมี:

• ไลบรารีสนับสนุน distsys ซึ่งใช้โดยรหัส GO ที่สร้างขึ้นของ PGO ของ PGO ซึ่งมีอยู่ใน distsys/ Folder
• ระบบที่สร้างขึ้นโดยใช้ PGO ใน systems/ โฟลเดอร์รวมถึงร้านค้าคีย์-ค่าตามแพ
• โหมดการเน้นไวยากรณ์สำหรับรหัส Visual Studio และ pygments มีอยู่ใน syntax/ โฟลเดอร์

คุณสามารถอ่านเพิ่มเติมเกี่ยวกับแง่มุมการวิจัยของงานของเราในกระดาษ Asplos'23 ของเราสำเนาซึ่งรวมอยู่ในที่เก็บนี้ การประเมินผลงาน Artifact ที่โดดเด่นของ PGO ของเราในการประชุมครั้งนั้น?

นอกจากนี้เรายังมีวิดีโอสองสามรายการที่คุณสามารถรับชมได้:

• PGO TLA+ Talk Conference, กันยายน 2022
• PGO ภาพรวมการพูดคุย, กุมภาพันธ์ 2022

จุดประสงค์และแรงจูงใจ

Pluscal เป็นภาษาสำหรับการระบุ/สร้างแบบจำลองระบบพร้อมกัน มันถูกออกแบบมาเพื่อให้ง่ายต่อการเขียน TLA+ โดยเฉพาะอย่างยิ่ง PlusCal สามารถรวบรวมเป็น TLA+ซึ่งสามารถตรวจสอบกับคุณสมบัติของระบบที่มีประโยชน์ (โดยใช้ตัวตรวจสอบโมเดล TLC) ตัวอย่างเช่นนี่คือพื้นที่เก็บข้อมูลของสูตรบวกกับการแก้ปัญหาเพื่อแก้ไขปัญหาการยกเว้นซึ่งกันและกัน

GO เป็นภาษาที่ใช้ C ที่พัฒนาโดย Google สำหรับการสร้างระบบกระจาย มันได้สร้างการสนับสนุนสำหรับการเกิดขึ้นพร้อมกันกับช่องทางและ goroutines ซึ่งทำให้ดีสำหรับการพัฒนาระบบกระจาย

ขณะนี้ไม่มีเครื่องมือที่สอดคล้องกับสเป็ค Pluscal/TLA+ กับการใช้งานของข้อมูลจำเพาะ PGO เป็นเครื่องมือที่มีจุดมุ่งหมายในการเชื่อมต่อข้อกำหนดกับการใช้งานโดยการสร้างรหัส GO ตามข้อกำหนดที่เขียนขึ้นใน Modular PlusCal คำนำหน้า "โมดูลาร์" มาจากความต้องการที่จะแยกแยะคำอธิบายของระบบจากแบบจำลองของสภาพแวดล้อมซึ่งจำเป็นสำหรับการตรวจสอบแบบจำลอง PGO ช่วยให้การแปลคำอธิบายแบบโมดูลาร์บวกกับระบบกระจายไปยัง PlusCal ที่ตรวจสอบได้รวมถึงโปรแกรม GO ที่เทียบเท่ากับความหมาย

สถานะปัจจุบัน

ภายใต้การพัฒนาอย่างแข็งขัน PGO รองรับการรวบรวมโครงสร้างการควบคุมการควบคุมบวกทั้งหมด PGO ยังสนับสนุน TLA+ ระดับมูลค่าส่วนใหญ่ที่สนับสนุนโดย TLC ดูคำขอดึงและปัญหาสำหรับเอกสารของงานต่อเนื่อง

ในสถานะการพัฒนาที่ใช้งานอยู่เราไม่ได้จัดเตรียมการเผยแพร่ที่มั่นคง ในการเรียกใช้ PGO วิธีที่ดีที่สุดคือโคลนพื้นที่เก็บข้อมูลและในสาขาหลักรันผ่านเครื่องมือสร้าง SBT:

 $ sbt
> run [command-line arguments]

ดูบันทึกการใช้งานด้านล่างสำหรับข้อโต้แย้งที่โปรแกรมยอมรับ หมายเหตุ: หากคุณเรียกใช้ในบรรทัดเดียวคุณจะต้องอ้างอิงอาร์กิวเมนต์เช่นเดียวกับใน sbt run "[command-line arguments]"

การใช้งาน

หากต้องการเรียนรู้วิธีใช้ PGO ในระหว่างการตรวจสอบดูหน้าการใช้งาน PGO (คำเตือน: อัปเดตระหว่างดำเนินการ)

สำหรับโหมดการรวบรวมและธงของเครื่องมือในระดับสูงดูด้านล่าง

ข้อความความช่วยเหลือของเครื่องมือ PGO อ่าน:

 PGo compiler
  -h, --help   Show help message

Subcommand: gogen
  -o, --out-file  <arg>
  -p, --package-name  <arg>
  -s, --spec-file  <arg>
  -h, --help                  Show help message

Subcommand: pcalgen
  -s, --spec-file  <arg>
  -h, --help               Show help message

ผู้ที่ได้รับความนิยม

คำสั่งย่อยของ gogen ร้องขอให้ PGO สร้างไฟล์ GO จากโมดูล TLA+ ที่มี MPCAL การปรับแต่งส่วนใหญ่ของขั้นตอนนี้ควรทำโดยเลือกพารามิเตอร์เฉพาะเมื่อเรียกรหัส GO ที่สร้างขึ้นดังนั้นจึงมีตัวเลือกเพียงไม่กี่ตัวที่ต้องพิจารณา

• --out-file ระบุเส้นทางไปยังไฟล์เอาต์พุต GO เช่น -o ใน GCC
• --spec-file ระบุเส้นทางไปยังไฟล์ TLA+ Input
• --package-name อนุญาตให้ปรับแต่งชื่อแพ็คเกจของไฟล์เอาต์พุต GO ค่าเริ่มต้นนี้เป็นชื่ออัลกอริทึม MPCAL เวอร์ชันที่ถูกฆ่าเชื้อ

pcalgen

คำสั่งย่อยของ pcalgen ร้องขอให้ PGO เขียนไฟล์ TLA+ ที่ประกอบด้วย MPCAL ใหม่ซึ่งมีการแปลบวกกับอัลกอริทึม MPCAL ตัวเลือกเดียว --spec-file คือเส้นทางไปยังไฟล์ Spec ซึ่งจะถูกเขียนใหม่

ในการแทรกการแปล Pluscal PGO จะค้นหาความคิดเห็นเช่นให้หรือใช้ช่องว่าง:

 * BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION

หากไม่พบหนึ่งในความคิดเห็นทั้งสองนี้ในลำดับนั้นมันจะยอมแพ้กับข้อความแสดงข้อผิดพลาดที่อธิบายถึงปัญหาและจะไม่เขียนผลลัพธ์ใด ๆ

มันทำงานอย่างไร

PGO เป็นแหล่งที่มาของคอมไพเลอร์แหล่งที่เขียนใน Scala มันรวบรวมข้อมูลจำเพาะที่เขียนไว้ในส่วนขยายของ Pluscal เรียกว่า Modular Pluscal (ดูหน้า Modular Pluscal สำหรับรายละเอียดเพิ่มเติม) เพื่อไปโปรแกรม

วิธีการสร้าง (เพื่อการพัฒนา)

รหัส SCALA ของ PGO สร้างผ่านโครงการ SBT โดยมีการอ้างอิงโดย Maven PGO ยังมีห้องสมุดสนับสนุนรันไทม์สำหรับรหัส GO ที่สร้างขึ้นซึ่งอาศัยอยู่ใน distsys/ Subfolder รหัส GO นี้เป็นโมดูล GO มาตรฐานซึ่งสามารถนำเข้าผ่าน URL https://github.com/distcompiler/pgo/distsys

สคริปต์การสร้างหลักคือ Build.sbt ระดับบนสุด ในการสร้างจากเทอร์มินัลให้เรียกใช้ sbt ในไดเรกทอรีรูทและใช้คำสั่งมาตรฐานที่จัดทำโดยคอนโซล SBT สิ่งเหล่านี้รวมถึง run <command-line args> ถึง (re-) คอมไพล์และเรียกใช้ PGO และ test เพื่อเรียกใช้การทดสอบทั้งหมดรวมถึงการทดสอบ GO (สิ่งที่ต้องทำ: เพิ่มนักวิ่งสำหรับการทดสอบ GO แบบยืนฟรีโดยเฉพาะอย่างยิ่งหายไป)

การสร้าง SBT ยังสามารถนำเข้าโดยอัตโนมัติโดยปลั๊กอิน Intellij Scala รวมถึง IDE อื่น ๆ ที่มีการสนับสนุน Scala

รหัส Scala ของ PGO มีการจัดการการพึ่งพาในชุดห้องสมุดยูทิลิตี้ชุดเล็ก ๆ :

• หอยเชลล์สำหรับการแยกอนุรักษ์บรรทัดคำสั่งการแยกวิเคราะห์
• Scala-Parser-combinators สำหรับตัวแยกวิเคราะห์ TLA+/PCAL/MPCAL
• OS-LIB สำหรับไฟล์และการจัดการกระบวนการง่าย ๆ (ใช้การจัดการกระบวนการในระหว่างการทดสอบ)

ชุดทดสอบของ PGO นอกจากนี้ขึ้นอยู่กับ:

• go ปฏิบัติการได้ การทดสอบจะพยายามค้นหาสิ่งนี้อาจอยู่บน $PATH หรือเทียบเท่าผ่านกระบวนการค้นหาเริ่มต้นของ JVM
• Scalatest เป็นกรอบทดสอบ
• Scalacheck สำหรับการใช้การทดสอบ Fuzz
• java-diff-utils สำหรับการสร้าง diffs เมื่อการทดสอบเปรียบเทียบบล็อกขนาดใหญ่ของข้อความ

ห้องสมุดรันไทม์ของ PGO ขึ้นอยู่กับ:

• ไม่เปลี่ยนรูปสำหรับการใช้งานรายการและแผนที่ที่ไม่เปลี่ยนแปลงอย่างมีประสิทธิภาพในรูปแบบข้อมูล TLA+ ตัวอย่างเช่นการสร้างแผนที่ที่แก้ไขด้วยคู่คีย์-ค่าที่แตกต่างกันควรใช้เวลาคงที่แทนที่จะคัดลอกโครงสร้างทั้งหมดที่มีอยู่
• Multierr สำหรับการรวมข้อผิดพลาด

PGO ได้รับการทดสอบโดยใช้ OpenJDK 1.11 ถึง 1.16 และไป 1.18 จำเป็นต้องใช้ OpenJDK 1.11+ เนื่องจากการใช้ API มาตรฐาน GO> = 1.18 เป็นสิ่งจำเป็นเนื่องจากทั่วไป