In concurrent systems in which user programs concurrently share resources, a synchronizer controls the accesses to a shared resource. Since the concurrent system performs its functions correctly, it is highly desirable to develop some means to produce the synchronizer as correct as possible. An automatic synthesis synchronizer is proposed as a tool which will aid the development of correct user programs.
In this thesis, an automatic synthesis system that translates specification language into Path Pascal is designed and implemented. Input to the system is represented using Ramamritham's SYSL: specifications of the shared resource, operations on the resource, and synchronization requirements. these specifications are translated into Path Pascal. The mapping methods that preserve the meanings of the specifications are used to synthesize systematically codes of the synchronizer from the given specifications.
